proposition: Lemma anga_is_ang : forall a, Q_CongA_Acute a -> Q_CongA a.
proof: Proof. intros. unfold Q_CongA_Acute in H. unfold Q_CongA. ex_and H A. ex_and H0 B. ex_and H C. exists A. exists B. exists C. apply acute_distincts in H. spliter. split. auto. split. auto. intros. split. intro. assert(Ang X Y Z a). unfold Ang. split. unfold Q_CongA. exists A. exists B. exists C. split. assumption. split. assumption. auto. assert(HH:= H0 X Y Z). apply HH. auto. unfold Ang in H3. spliter. auto. intro. apply H0. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length