proposition: Lemma mod2sub: forall a b, b <= a -> mod2 (a - b) = xorb (mod2 a) (mod2 b).
proof: Proof. intros. remember (a - b) as c. revert dependent b. revert a. revert c. change (forall c, (fun c => forall a b, b <= a -> c = a - b -> mod2 c = xorb (mod2 a) (mod2 b)) c). apply strong. intros c IH a b AB N. destruct c. - assert (a=b) by lia. subst. rewrite Bool.xorb_nilpotent. reflexivity. - destruct c. + assert (a = S b) by lia. subst a. simpl (mod2 1). rewrite mod2_S_not. destruct (mod2 b); reflexivity. + destruct a; [lia|]. destruct a; [lia|]. simpl. apply IH; lia. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Bool.Bool Coq.Arith.Arith Coq.micromega.Lia Coq.NArith.NArith Coq.ZArith.ZArith bbv.N_Z_nat_conversions bbv.Nomega