proposition: Lemma anga_acute : forall a A B C , Q_CongA_Acute a -> a A B C -> Acute A B C.
proof: Proof. intros. unfold Q_CongA_Acute in H. ex_and H A0. ex_and H1 B0. ex_and H C0. assert(HH:= acute_lea_acute A B C A0 B0 C0). apply HH. auto. unfold LeA. exists C0. split. unfold InAngle. apply acute_distincts in H. spliter. repeat split; auto. exists C0. split. Between. right. apply out_trivial. auto. assert(HP:= H1 A B C). destruct HP. apply conga_sym. apply H3. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid