proposition: Lemma lcos_eqa_lcos : forall lp l a b, Lcos lp l a -> EqA a b -> Lcos lp l b.
proof: Proof. intros. assert(HH:=lcos_lg_anga l lp a H). spliter. clear H1. assert(HH:= H0). unfold EqA in HH. assert (Q_CongA a) by (apply anga_is_ang;auto). assert (Q_CongA b) by (apply eqA_preserves_ang with a;auto). assert (Q_CongA_Acute b). apply (eqA_preserves_anga a b); auto. unfold Lcos in *. spliter. repeat split; auto. ex_and H9 A. ex_and H10 B. ex_and H9 C. exists A. exists B. exists C. repeat split; auto. apply HH;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms