proposition: Lemma lcos3_eq_sym : forall l1 a b c l2 d e f, Eq_Lcos3 l1 a b c l2 d e f -> Eq_Lcos3 l2 d e f l1 a b c.
proof: Proof. intros. unfold Eq_Lcos3 in *. ex_and H lp. exists lp. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms