proposition: Lemma nat_to_group_inverse : forall (n : nat) (r : G), Equal (group_inverse G (nat_to_group r n)) (nat_to_group (group_inverse G r) n).
proof: Proof. simple induction n; simpl in |- *; auto with *. intros n0 H' r0; try assumption. apply Trans with (sgroup_law G (group_inverse G r0) (group_inverse G (nat_to_group r0 n0))); auto with *. apply Trans with (sgroup_law G (group_inverse G r0) (nat_to_group (group_inverse G r0) n0)); auto with *. Qed.
imports: Zring Group_kernel