proposition: Lemma lcos2_eq_refl : forall l a b, Q_Cong l -> ~ Q_Cong_Null l -> Q_CongA_Acute a -> Q_CongA_Acute b -> Eq_Lcos2 l a b l a b.
proof: Proof. intros. assert(HH:= lcos2_exists l a b H H0 H1 H2). ex_and HH lab. unfold Eq_Lcos2. exists lab. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms