proposition: Lemma Z_to_group_fun_eq : forall z : ZZ, Equal (Z_to_group_fun z) (Z_to_group_nat r z).
proof: Proof. intros z; simpl in |- *. unfold Z_to_group_fun in |- *. unfold Z_to_group_nat_fun in |- *. case (Z_gt_le_dec z 0); intros z0. auto with *. case (Z_le_lt_eq_dec z 0 z0); intros z1. apply Trans with (nat_to_group (group_inverse G r) (nat_of_P (pos_abs (Zlemma1 z1)))); auto with *. auto with *. Qed.
imports: Zring Group_kernel