proposition: Theorem rltTrans : transitive rNat rlt.
proof: Proof. red in |- *; unfold rlt in |- *; intros x y z H1 H2. apply nat_of_P_lt_Lt_compare_complement_morphism. apply Nat.lt_trans with (nat_of_P y); apply nat_of_P_lt_Lt_compare_morphism; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)