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