proposition: Theorem Rlt_nge : forall n m : R, n < m <-> ~ m <= n.
proof: Proof. intros n m; split. - intros H H1; assert (H2 : n < n) by now apply Rlt_le_trans with m. now apply (Rlt_neq H2). - intro H. destruct (Rle_gt_cases m n) as [H1 | H1]. + false_hyp H1 H. + assumption. Qed.
imports: Setoid Ring