proposition: Lemma Smallest_less_Average : forall a b : R, a [<] b -> a [<] (a[+]b) [/]TwoNZ.
proof: Proof. intros. apply shift_less_div. apply pos_two. rstepl (a[+]a). apply plus_resp_less_lft. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)