proposition: Lemma adde_lem_gen x1 x2 y1 y2 z1 z2 (e1 : y1 ^+ 2 * z1 = x1 ^+ 3 + A * x1 * z1 ^+ 2 + B * z1 ^+ 3) (e2 : y2 ^+ 2 * z2 = x2 ^+ 3 + A * x2 * z2 ^+ 2 + B * z2 ^+ 3) : let d1 := x2 * z1 in let d2 := x1 * z2 in let l := d1 - d2 in let dl := d1 + d2 in let m := y2 * z1 - y1 * z2 in let l2 := l * l in let l3 := l2 * l in let m2 := m * m in let x3 := z1 * z2 * m2 - l2 * dl in (z2 * l2 * (m * x1 - y1 * l) - m * x3) ^+ 2 * (z1 * z2 * l3) = (l * x3) ^+ 3 + A * (l * x3) * (z1 * z2 * l3) ^+ 2 + B * (z1 * z2 * l3) ^+ 3.
proof: Proof. by ring: e1 e2. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)