proposition: Lemma pos_one : ([0]:R) [<] [1].
proof: Proof. elim (ap_imp_less _ _ _ (ring_non_triv R)). 2: auto. intro H. exfalso. apply (less_irreflexive_unfolded R [1]). apply less_transitive_unfolded with ([0]:R). auto. cut (([0]:R) [<] [--][1]). 2: astepl (([1]:R)[+][--][1]). 2: astepr (([0]:R)[+][--][1]). 2: apply plus_resp_less_rht; auto. intro H0. rstepr ([--]([1]:R)[*][--][1]). apply (mult_resp_pos _ _ _ H0 H0). Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)