proposition: Theorem ppow_1: forall n, ppow (1, 0) n = (1, 0).
proof: Proof. intros n; case n; simpl; auto. intros p; apply iter_pos_invariant with (Inv := fun x => x = (1, 0)); auto. intros x H; rewrite H; auto. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup