fact: Definition pe2e (p : pelt) := let (x, y, z, e) := p in let (b, p) := wb (z == 0) in (if b then fun=> inf_elt A B else fun p1 : (z == 0) = false => curve_elt (pe2e_lem1 e p1)) p.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)