chore(proofs): add F* corpus (5 arithmetic lemmas)

AddComm, AddAssoc, MulZero, NonNeg, Refl — all discharged by F*'s
SMT backend. Exercises the fstar runner in batch_driver.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/fstar/AddAssoc.fst

@@ -0,0 +1,3 @@
+module AddAssoc
+val add_assoc : x:int -> y:int -> z:int -> Lemma ((x + y) + z == x + (y + z))
+let add_assoc _ _ _ = ()

proofs/fstar/AddComm.fst

@@ -0,0 +1,3 @@
+module AddComm
+val add_comm : x:int -> y:int -> Lemma (x + y == y + x)
+let add_comm _ _ = ()

proofs/fstar/MulZero.fst

@@ -0,0 +1,4 @@
+module MulZero
+open FStar.Mul
+val mul_zero : x:int -> Lemma (x * 0 == 0)
+let mul_zero _ = ()

proofs/fstar/NonNeg.fst

@@ -0,0 +1,3 @@
+module NonNeg
+val abs_nonneg : x:int -> Lemma (if x >= 0 then x >= 0 else -x >= 0)
+let abs_nonneg _ = ()

proofs/fstar/Refl.fst

@@ -0,0 +1,3 @@
+module Refl
+val refl : x:int -> Lemma (x == x)
+let refl _ = ()