proposition: Lemma anga_distincts : forall a A B C, Q_CongA_Acute a -> a A B C -> A <> B /\ C <> B.
proof: Proof. intros. assert(HH:= ex_lg A B). ex_and HH la. assert(HH:= ex_lg C B). ex_and HH lc. assert(HH:= anga_not_null_lg a la A B C H H1 H0 H2). assert(a C B A). apply anga_sym; auto. assert(HQ:= anga_not_null_lg a lc C B A H H3 H5 H4). split; intro; subst B. apply HH. unfold Q_Cong_Null. split. auto. exists A. auto. apply HQ. unfold Q_Cong_Null. split. auto. exists C. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid