proposition: Lemma Zcleb_morph : forall x y : Z, Z.leb x y = true -> [x] <= [y].
proof: Proof. unfold Z.leb; intros x y H. case_eq (x ?= y)%Z; intro H1; rewrite H1 in H. - le_equal. apply (morph_eq Zring_morph). unfold Zeq_bool; now rewrite H1. - le_less. now apply clt_morph. - discriminate. Qed.
imports: OrderedRing RingMicromega ZArith_base InitialRing Setoid ZArithRing