proposition: Lemma lcos3_permut2 : forall lp l a b c, Lcos3 lp l a b c -> Lcos3 lp l c b a.
proof: Proof. intros. apply lcos3_permut3. apply lcos3_permut1. apply lcos3_permut3. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms