proposition: Lemma add_lem_tan: forall x1 y1 z1 (H1 : y1 ^ 2 * z1 = x1 ^ 3 + A * x1 * z1 ^ 2 + B * z1 ^ 3), let m := 3 * x1 * x1 + A * z1 * z1 in let l := 2 * y1 * z1 in let m2 := m * m in let l2 := l * l in let l3 := l2 * l in let x3 := m2 * z1 - 2 * x1 * l2 in (l2 * (m * x1 - y1 * l) - m * x3) ^ 2 * (z1 * l3) = (l * x3) ^ 3 + A * (l * x3) * (z1 * l3) ^ 2 + B * (z1 * l3) ^ 3.
proof: Proof. intros x1 y1 z1 H1 m l m2 l2 l3 x3. unfold x3, l3, l2, m2, l, m. apply Keq_minus_eq. ring [H1]. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith