proposition: Lemma Zneq_bool_true: forall x y, Zneq_bool x y=true -> x<>y.
proof: Proof. intros x y; unfold Zneq_bool. intros H H0; subst. rewrite Z.compare_refl in H. discriminate. Qed.
imports: ZArith Znumtheory hoarelogic Zwf Wellfounded Lia