fact: Definition B (x : GroupElement) := [c, p1, p2] <-$3 A x; [v1, r1] <-2 p1; [v2, r2] <-2 p2; ret (modNat ((v1 + (modNatAddInverse v2 order)) * (multInverseModOrder (r2 + (modNatAddInverse r1 order)))) order)%nat.
imports: FCF GroupTheory OTP RndNat RndGrpElem