proposition: Lemma add_lem_gen: forall x1 x2 y1 y2 z1 z2 (H1 : y1 ^ 2 * z1 = x1 ^ 3 + A * x1 * z1 ^ 2 + B * z1 ^ 3) (H2 : 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. intros x1 x2 y1 y2 z1 z2 H1 H2 d1 d2 l dl m l2 l3 m2 x3. unfold x3, m2, l3, l2, m, dl, l, d1, d2. apply Keq_minus_eq. ring [H1 H2]. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith