proposition: Lemma Average_less_Greatest : forall a b : R, a [<] b -> (a[+]b) [/]TwoNZ [<] b.
proof: Proof. intros. apply shift_div_less'. apply pos_two. rstepr (b[+]b). apply plus_resp_less_rht. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)