proposition: Lemma affineAffine_r : forall a b o1 o2, (affineCombo o1 (affineCombo o2 a b) b==affineCombo (o1*o2) a b)%Q.
proof: Proof. intros a b o1 o2. unfold affineCombo. simpl. ring. Qed.
imports: Coq.QArith.QArith CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields CoRN.tactics.Qauto CoRN.tactics.CornTac