proposition: Lemma Plt_lt (p q: positive): Pos.lt p q <-> (nat_of_P p < nat_of_P q).
proof: Proof. split. apply nat_of_P_lt_Lt_compare_morphism. apply nat_of_P_lt_Lt_compare_complement_morphism. Qed.
imports: Coq.Setoids.Setoid Coq.PArith.BinPos Coq.PArith.Pnat ZArith_base