proposition: Lemma OMEGA10 v c1 c2 l1 l2 k1 k2 : (v * c1 + l1) * k1 + (v * c2 + l2) * k2 = v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2).
proof: Proof. rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc. rewrite <- !Z.add_assoc. f_equal. apply Z.add_shuffle3. Qed.
imports: BinInt Znat