proposition: Lemma lcos_eq_refl : forall la a, Q_Cong la -> ~ Q_Cong_Null la -> Q_CongA_Acute a -> Eq_Lcos la a la a.
proof: Proof. intros. unfold Eq_Lcos. assert(HH:=lcos_exists la a H1 H H0). ex_and HH lp. exists lp. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms