proposition: Lemma Zl4 : forall p p0 : positive, Equal (Z_to_group_nat_fun (Zpos p + Zneg p0)%Z) (sgroup_law G (nat_to_group (nat_of_P p)) (group_inverse G (nat_to_group (nat_of_P p0)))).
proof: Proof. intros p p0; try assumption. case (Z_gt_le_dec (Zpos p) (Zpos p0)); intros z. rewrite ax5; auto with *. apply Trans with (nat_to_group (nat_of_P (pos_abs (ax3 (p - p0))))); auto with *. simpl in |- *. rewrite nat_of_P_minus_morphism; auto with *. apply nat_to_group_minus. apply nat_of_P_gt_Gt_compare_morphism. auto with *. case (Z_le_lt_eq_dec _ _ z); intros. rewrite ax6; auto with *. apply Trans with (group_inverse G (nat_to_group (nat_of_P (pos_abs (ax3 (p0 - p)))))); auto with *. simpl in |- *. rewrite nat_of_P_minus_morphism; auto with *. apply Trans with (group_inverse G (sgroup_law G (nat_to_group (nat_of_P p0)) (group_inverse G (nat_to_group (nat_of_P p))))); auto with *. apply GROUP_comp. apply nat_to_group_minus. apply nat_of_P_gt_Gt_compare_morphism. auto with *. apply Trans with (sgroup_law G (group_inverse G (group_inverse G (nat_to_group (nat_of_P p)))) (group_inverse G (nat_to_group (nat_of_P p0)))); auto with *. injection e. intros H'; try assumption. rewrite <- H'. rewrite ax7. apply Trans with (monoid_unit G); auto with *. Qed.
imports: Zring Group_kernel