proposition: Lemma lcos3_permut3 : forall lp l a b c, Lcos3 lp l a b c -> Lcos3 lp l b a c.
proof: Proof. intros. assert(HH:= lcos3_lcos_2_1 lp l a b c). destruct HH. assert(exists lab : Tpoint -> Tpoint -> Prop, Lcos2 lab l a b /\ Lcos lp lab c). apply lcos3_lcos_2_1; auto. ex_and H2 lab. apply lcos2_comm in H2. apply lcos3_lcos_2_1. exists lab. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms