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