proposition: Lemma Assoc_PA : Assoc_law Comp_PA.
proof: Proof. unfold Assoc_law in |- *. intros x y z o4 f; elim f. intros g h. apply Trans with (Comp_PA_mor g h). apply (Comp_PA_fact1 PA_I1 (Comp_PA_mor g h)). apply (Comp_PA_congr (f:=g) (g:=Comp_PA_mor PA_I1 g) h). apply Sym. apply (Comp_PA_fact1 PA_I1 g). intros g h. apply Trans with (Comp_PA_mor g h). apply (Comp_PA_fact2 PA_I2 (Comp_PA_mor g h)). apply (Comp_PA_congr (f:=g) (g:=Comp_PA_mor PA_I2 g) h). apply Sym. apply (Comp_PA_fact2 PA_I2 g). intro i; elim z. intros g h; apply (PA_21_ind (fun x : PA_mor PA2 PA1 => Comp_PA_mor (PA_f i) (Comp_PA_mor g h) =_S Comp_PA_mor (Comp_PA_mor (PA_f i) g) h) g). intros g h; apply Trans with (Comp_PA_mor (PA_f i) h). apply (Comp_PA_congl (f:=Comp_PA_mor g h) (g:=h) (PA_f i)). apply (Comp_PA_fact2 g h). simpl in |- *. apply (Comp_PA_congr (f:=PA_f i) (g:=Comp_PA_mor (PA_f i) g) h). apply Sym. apply (Comp_PA_fact3 i g). Qed.
imports: BasicTypes Category