proposition: Lemma Zl1 : Equal (Z_to_group_nat_fun 0%Z) (monoid_unit G).
proof: Proof. unfold Z_to_group_nat_fun in |- *. case (Z_gt_le_dec 0 0). intros z; try assumption. absurd (0 > 0)%Z; auto with *. intros z; try assumption. case (Z_le_lt_eq_dec 0 0 z). intros z0; try assumption. absurd (0 < 0)%Z; auto with *. auto with *. Qed.
imports: Zring Group_kernel