proposition: Lemma Zl5 : Equal (Z_to_group_nat_fun (ring_unit ZZ)) r.
proof: Proof. unfold Z_to_group_nat_fun in |- *. case (Z_gt_le_dec (ring_unit ZZ) 0). intros z; try assumption. simpl in |- *. auto with *. intros z; try assumption. case (Z_le_lt_eq_dec (ring_unit ZZ) 0 z). intros z0; try assumption. absurd (ring_unit ZZ < 0)%Z; auto with *. intros H'; try assumption. inversion H'. Qed.
imports: Zring Group_kernel