proposition: Lemma pos_nat_group : forall p : positive, Equal (pos_to_group p) (nat_to_group r (nat_of_P p)).
proof: Proof. simple induction p; simpl in |- *. intros p0 H'; try assumption. rewrite ZL6. unfold group_square in |- *. apply Trans with (sgroup_law G (sgroup_law G (nat_to_group r (nat_of_P p0)) (nat_to_group r (nat_of_P p0))) r); auto with *. unfold group_square in |- *. intros p0 H'; try assumption. unfold nat_of_P in |- *. simpl in |- *. rewrite ZL6. apply Trans with (sgroup_law G (nat_to_group r (nat_of_P p0)) (nat_to_group r (nat_of_P p0))); auto with *. auto with *. Qed.
imports: Zring Group_kernel