proposition: Theorem Qnat_lt : ∀ i j, (i < j)%nat ↔ Qnat i < Qnat j.
proof: Proof. intros i j; split; intros H. unfold Qnat, Qlt; simpl. do 2 rewrite Zmult_1_r. apply inj_lt; assumption. unfold Qlt in H; simpl in H. do 2 rewrite Z.mul_1_r in H. apply Nat2Z.inj_lt in H; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz