proposition: Lemma Z_group_nat_fun_mult_pos : forall (p q : positive) (g : G), Equal (Z_to_group_nat_fun g (Zpos p * Zpos q)%Z) (Z_to_group_nat_fun (Z_to_group_nat_fun g (Zpos p)) (Zpos q)).
proof: Proof. simpl in |- *. intros p q g; try assumption. apply Trans with (nat_to_group g (nat_of_P (pos_abs (ax3 ((fun (x : positive) (_ : positive -> positive) (y : positive) => (x * y)%positive) p (fun y : positive => y) q))))); auto with algebra. apply Trans with (nat_to_group (Z_to_group_nat_fun g (Zpos p)) (nat_of_P (pos_abs (ax3 q)))); auto with algebra. simpl in |- *. rewrite (fun (x y : positive) (_ : positive -> positive) => nat_of_P_mult_morphism x y). apply Trans with (nat_to_group (nat_to_group g (nat_of_P p)) (nat_of_P q)); auto with algebra. Qed.
imports: Z_group