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