proposition: Lemma Zneq_bool_false: forall x y, Zneq_bool x y=false -> x=y.
proof: Proof. intros x y H0; apply Zcompare_Eq_eq; generalize H0; clear H0; unfold Zneq_bool. case (x ?= y)%Z; auto; try (intros; discriminate); auto. Qed.
imports: ZArith Znumtheory hoarelogic Zwf Wellfounded Lia