proposition: Lemma adde_lem_tan x1 y1 z1 (e1 : y1 ^ 2 * z1 = x1 ^ 3 + A * x1 * z1 ^ 2 + B * z1 ^ 3) : let m := 3%:R * x1 * x1 + A * z1 * z1 in let l := 2%:R * y1 * z1 in let m2 := m * m in let l2 := l * l in let l3 := l2 * l in let x3 := m2 * z1 - 2%:R * 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. by ring: e1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)