fact: Fixpoint psplit l: positive * (List.list positive) := match l with List.nil => (xH, List.nil) | List.cons (a, xH) l1 => let (v, l2) := psplit l1 in (v, (List.cons a l2)) | List.cons (a, n) l1 => let (v, l2) := psplit l1 in (Pmult (Ppow a (Pos.pred n)) v, (List.cons a l2)) end.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod