proposition: Lemma lcos3_eql_lcos3 : forall lla llb la lb a b c, Lcos3 la lla a b c -> EqL lla llb -> EqL la lb -> Lcos3 lb llb a b c.
proof: Proof. intros. unfold Lcos3 in *. ex_and H lpa. exists lpa. ex_and H2 lpab. exists lpab. apply lcos_lg_anga in H. apply lcos_lg_anga in H2. apply lcos_lg_anga in H3. spliter. split. rewrite <- H0;auto. split. auto. rewrite <- H1;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms