proposition: Lemma Lp_coUAlaw1 : Limit_law1 (Limiting_cone l o_C G) Lp_diese.
proof: Proof. unfold Limit_law1, Limit_eq in |- *; simpl in |- *; intros d tau i. unfold Comp_cone_tau, Lp_diese in |- *. apply Trans with (ApAphi la (Lim_diese l (Lp_sigma tau) o Limiting_cone l i)). apply Sym. apply (Adj_eq3 la (Limiting_cone l i) (Lim_diese l (Lp_sigma tau))). apply Trans with (ApAphi la (ApAphi_inv (c:=H i) la (tau i))). unfold Comp_FOb in |- *; apply AphiPres. apply (Prf_limit1 l (Lp_sigma tau) i). apply (Idl_inv (NTa_areIso la (Build_POb1 d (H i))) (tau i)). Qed.
imports: Adj_UA Pres_Limits