proposition: Lemma lcos3_eq_refl : forall l a b c, Q_Cong l -> ~ Q_Cong_Null l -> Q_CongA_Acute a -> Q_CongA_Acute b -> Q_CongA_Acute c -> Eq_Lcos3 l a b c l a b c.
proof: Proof. intros. assert(HH:= lcos3_exists l a b c H H0 H1 H2 H3). ex_and HH lp. unfold Eq_Lcos3. exists lp. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms