fact: Definition padd := fun p1 p2: pelt => let (x1, y1, z1, H1) := p1 in if (is_zero z1) then p2 else let (x2, y2, z2, H2) := p2 in if (is_zero z2) then p1 else 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 if (l ?= 0) then if (m ?= 0) then let m' := 3 * x1 * x1 + A * z1 * z1 in let l' := 2 * 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 * x1 * l'2 in @mk_pelt (l' * x3) (l'2 * (m' * x1 - y1 * l') - m' * x3) (z1 * l'3) (add_lem_tan H1) else @mk_pelt 0 1 0 add_lem0 else let l2 := l * l in let l3 := l2 * l in let m2 := m * m in let x3 := z1 * z2 * m2 - l2 * dl in @mk_pelt (l * x3) (z2 * l2 * (m * x1 - y1 * l) - m * x3) (z1 * z2 * l3) (add_lem_gen H1 H2).
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith