proposition: Theorem Rlt_trans : forall n m p : R, n < m -> m < p -> n < p.
proof: Proof. intros n m p; repeat rewrite Rlt_le_neq; intros [H1 H2] [H3 H4]; split. - now apply Rle_trans with m. - intro H. rewrite H in H1. pose proof (Rle_antisymm H3 H1). now apply H4. Qed.
imports: Setoid Ring