proposition: Theorem Rle_lt_eq : forall n m : R, n <= m <-> n < m \/ n == m.
proof: Proof. intros n m; rewrite Rlt_le_neq. split; [intro H | intros [[H1 H2] | H]]. - destruct (Req_em n m) as [H1 | H1]. + now right. + left; now split. - assumption. - rewrite H; apply Rle_refl. Qed.
imports: Setoid Ring