proposition: Lemma Zcneqb_morph : forall x y : Z, Zeq_bool x y = false -> [x] ~= [y].
proof: Proof. intros x y H. unfold Zeq_bool in H. case_eq (Z.compare x y); intro H1; rewrite H1 in *; (discriminate || clear H). - apply (Rlt_neq sor). now apply clt_morph. - fold (x > y)%Z in H1. rewrite Z.gt_lt_iff in H1. apply (Rneq_symm sor). apply (Rlt_neq sor). now apply clt_morph. Qed.
imports: OrderedRing RingMicromega ZArith_base InitialRing Setoid ZArithRing