proposition: Lemma is_zero_correct: forall x y, if (x ?= y) then x = y else x <> y.
proof: Proof. intros x y; unfold Zeq_bool. case (Zcompare_Eq_iff_eq x y). case Z.compare; auto. intros _ H1 H2; assert (H3:= H1 H2); discriminate. intros _ H1 H2; assert (H3:= H1 H2); discriminate. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod