proposition: Lemma R_lt_irreflexive : irreflexive R_lt.
proof: Proof. red in |- *; intros x Hx. elim Hx; intros N HN. elim HN; clear Hx HN; intros e He HN. apply (ap_irreflexive_unfolded _ (x N)). apply less_imp_ap. apply less_leEq_trans with (x N[+]e). astepl (x N[+][0]); apply plus_resp_less_lft; auto. apply shift_plus_leEq'; auto with arith. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection