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