proposition: Lemma clt_morph : forall x y : Z, (x < y)%Z -> [x] < [y].
proof: Proof. intros x y H. do 2 rewrite (same_genZ (SORsetoid sor) ring_ops_wd (SORrt sor)); destruct x; destruct y; simpl in *; try discriminate. - apply phi_pos1_pos. - now apply clt_pos_morph. - apply <- (Ropp_neg_pos sor); apply phi_pos1_pos. - apply (Rlt_trans sor) with 0. + apply <- (Ropp_neg_pos sor); apply phi_pos1_pos. + apply phi_pos1_pos. - apply -> (Ropp_lt_mono sor); apply clt_pos_morph. red. now rewrite Pos.compare_antisym. Qed.
imports: OrderedRing RingMicromega ZArith_base InitialRing Setoid ZArithRing