proposition: Lemma lcos2_comm : forall lp l a b, Lcos2 lp l a b -> Lcos2 lp l b a.
proof: Proof. intros. unfold Lcos2 in *. ex_and H la. apply lcos_lg_anga in H. apply lcos_lg_anga in H0. spliter. assert(exists lb, Lcos lb l b). apply(lcos_exists l b); auto. assert(HH:= lcos_lg_not_null la l a H). tauto. ex_and H7 lb. apply lcos_lg_anga in H8. spliter. exists lb. split. auto. assert(exists lp', Lcos lp' lb a). apply(lcos_exists lb a); auto. assert(HH:= lcos_lg_not_null lb l b H7). tauto. ex_and H11 lp'. assert(EqL lp lp'). apply(l13_7 a b l la lb lp lp'); auto. apply lcos_lg_anga in H12. rewrite H11. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms