proposition: Theorem group_OTP_r : forall (x : GroupElement), comp_spec eq (RndG) (r <-$ RndG; ret (groupOp r x)).
proof: Proof. eapply OTP_inf_th_sec_r; intuition. apply associativity. eapply left_inverse. eapply right_inverse. eapply right_identity. eapply RndGrpElem_spec. Qed.
imports: FCF.FCF FCF.RndNat FCF.RndGrpElem