proposition: Lemma OMEGA15 v c1 c2 l1 l2 k2 : v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2).
proof: Proof. rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc. apply Z.add_shuffle1. Qed.
imports: BinInt Znat