proposition: Lemma eqA_preserves_anga : forall a b, Q_CongA_Acute a -> Q_CongA b -> EqA a b -> Q_CongA_Acute b.
proof: Proof. intros. assert (Q_CongA a). apply eqA_preserves_ang with b;auto. symmetry;auto. unfold EqA in H1. anga_instance a A B C. assert(HH:= H1 A B C). destruct HH. unfold Q_CongA_Acute. exists A. exists B. exists C. split. unfold Q_CongA_Acute in H. ex_and H A'. ex_and H6 B'. ex_and H C'. assert(a A' B' C'). assert(HP:= H6 A B C). destruct HP. assert(CongA A B C A' B' C') by (apply conga_sym;auto). assert(HP:=is_ang_conga_is_ang A B C A' B' C' a). assert(Ang A' B' C' a). apply HP. split; auto. auto. unfold Ang in H10. spliter. auto. apply (acute_lea_acute _ _ _ A' B' C'). auto. unfold LeA. exists C'. split. assert (HH:= acute_distincts A' B' C' H). spliter. apply inangle3123; auto. apply (is_ang_conga _ _ _ _ _ _ a). split; auto. split; auto. intros. split. intro. assert(HH:= H1 X Y Z). destruct HH. assert(Ang X Y Z a). eapply (is_ang_conga_is_ang A B C). split; auto. auto. unfold Ang in H9. spliter. auto. intro. assert(HH:= H1 X Y Z). destruct HH. assert(a X Y Z). auto. apply (is_ang_conga _ _ _ _ _ _ a). split; auto. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid