proposition: Lemma Z_to_group_nat_unit : forall n : Z, Equal (Z_to_group_nat_fun (monoid_unit G) n) (monoid_unit G).
proof: Proof. simple induction n; simpl in |- *; auto with algebra. intros p; try assumption. apply Trans with (nat_to_group (monoid_unit G) (nat_of_P (pos_abs (ax3 p)))); auto with algebra. intros p; try assumption. apply Trans with (group_inverse G (nat_to_group (monoid_unit G) (nat_of_P (pos_abs (ax3 p))))); auto with algebra. apply Trans with (group_inverse G (monoid_unit G)); auto with algebra. Qed.
imports: Z_group