proposition: Lemma Smod2_1: forall k, S k mod 2 = 1 -> k mod 2 = 0.
proof: Proof. intros k C. change (S k) with (1 + k) in C. rewrite Nat.add_mod in C by congruence. pose proof (Nat.mod_upper_bound k 2). assert (k mod 2 = 0 \/ k mod 2 = 1) as E by lia. destruct E as [E | E]; [assumption|]. rewrite E in C. simpl in C. discriminate. 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