proposition: Lemma R_one_ap_zero : R_one [#] [0].
proof: Proof. right; exists 0; exists ([1]:F). apply pos_one. intros; simpl in |- *; astepr ([1]:F); apply leEq_reflexive. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection