proposition: Lemma pos_two : ([0]:R) [<] Two.
proof: Proof. apply less_leEq_trans with ([1]:R). exact pos_one. apply less_leEq; exact one_less_two. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)