proposition: Lemma ang_not_lg_null : forall a la lc A B C, Q_Cong la -> Q_Cong lc -> Q_CongA a -> la A B -> lc C B -> a A B C -> ~ Q_Cong_Null la /\ ~ Q_Cong_Null lc.
proof: Proof. intros. assert(HH:=ang_distincts a A B C H1 H4). spliter. split. intro. unfold Q_Cong_Null in H7. spliter. ex_and H8 P. assert(HH:= lg_cong la A B P P H H2 H9). apply cong_identity in HH. contradiction. intro. unfold Q_Cong_Null in H7. spliter. ex_and H8 P. assert(HH:= lg_cong lc C B P P H0 H3 H9). apply cong_identity in HH. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid