proposition: Lemma is_null_all : forall a A B, A <> B -> Q_CongA_Null_Acute a -> a A B A.
proof: Proof. intros. unfold Q_CongA_Null_Acute in H0. spliter. assert(HH:= H0). unfold Q_CongA_Acute in HH. ex_and HH A0. ex_and H2 B0. ex_and H3 C0. apply acute_distincts in H2. spliter. apply H3. assert (a A0 B0 C0). apply H3. apply conga_refl; auto. assert(HH:= (H1 A0 B0 C0 H5)). apply l11_21_b; auto. apply out_trivial. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid