proposition: Lemma clt_pos_morph : forall x y : positive, (x < y)%positive -> phi_pos1 x < phi_pos1 y.
proof: Proof. intros x y H. pattern y; apply Pos.lt_ind with x. - rewrite phi_pos1_succ; apply (Rlt_succ_r sor). - clear y H; intros y _ H. rewrite phi_pos1_succ. now apply (Rlt_lt_succ sor). - assumption. Qed.
imports: OrderedRing RingMicromega ZArith_base InitialRing Setoid ZArithRing