axiom frac_Qinv2: \forall a,b:nat.Qinv(frac (Zopp a) b) = frac (Zopp b) a.
definition sigma_Q \def \lambda n,p,f.iter_p_gen n p Q f QO Qplus.
axiom frac_Qinv2: \forall a,b:nat.Qinv(frac (Zopp a) b) = frac (Zopp b) a.
definition sigma_Q \def \lambda n,p,f.iter_p_gen n p Q f QO Qplus.