proposition: Lemma affineCombo_gt : forall o a b (H:a < b), a < affineCombo o a b.
proof: Proof. intros o a b H. unfold affineCombo. rewrite -> Qlt_minus_iff in *. replace RHS with ((1-o)*(b-a)) by simpl; ring. apply: mult_resp_pos; simpl; auto with *. Qed.
imports: Coq.QArith.QArith CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields CoRN.tactics.Qauto CoRN.tactics.CornTac