proposition: Lemma od_inj a b: od a = od b -> a = b.
proof: Proof. revert b. induction a using nat_ind_2; intros [|[|b]]; simpl; trivial; (try (case od; discriminate)); (try discriminate). intro. f_equal. f_equal. apply IHa. revert H. case od. case od. congruence. Qed.
imports: List PeanoNat common comparisons