proposition: Lemma anga_not_lg_null : forall a la lc A B C, Q_Cong la -> Q_Cong lc -> Q_CongA_Acute a -> la A B -> lc C B -> a A B C -> ~ Q_Cong_Null la /\ ~ Q_Cong_Null lc.
proof: Proof. intros. apply anga_is_ang in H1. apply(ang_not_lg_null a la lc A B C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid