proposition: Theorem Rle_refl : forall n : R, n <= n.
proof: Proof. Proof (SORle_refl sor). Theorem Rle_antisymm : forall n m : R, n <= m -> m <= n -> n == m. Proof (SORle_antisymm sor). Theorem Rle_trans : forall n m p : R, n <= m -> m <= p -> n <= p. Proof (SORle_trans sor). Theorem Rlt_trichotomy : forall n m : R, n < m \/ n == m \/ m < n. Proof (SORlt_trichotomy sor). Theorem Rlt_le_neq : forall n m : R, n < m <-> n <= m /\ n ~= m. Proof (SORlt_le_neq sor). Theorem Rneq_0_1 : 0 ~= 1. Proof (SORneq_0_1 sor). Theorem Req_em : forall n m : R, n == m \/ n ~= m. Proof. intros n m. destruct (Rlt_trichotomy n m) as [H | [H | H]]; try rewrite Rlt_le_neq in H. - right; now destruct H. - now left. - right; apply Rneq_symm; now destruct H. Qed.
imports: Setoid Ring