fact: Definition pdouble (p1 : pelt) := let (x1, y1, z1, e1) := p1 in if z1 == 0 then p1 else let m' := 3%:R * x1 * x1 + A * z1 * z1 in let l' := 2%:R * y1 * z1 in let m'2 := m' * m' in let l'2 := l' * l' in let l'3 := l'2 * l' in let x3 := m'2 * z1 - 2%:R * x1 * l'2 in {| x := l' * x3; y := l'2 * (m' * x1 - y1 * l') - m' * x3; z := z1 * l'3; on_curve := adde_lem_tan e1 |}.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)