proposition: Lemma out_null_ang : forall a A B C, Q_CongA a -> a A B C -> Out B A C -> Q_CongA_Null a.
proof: Proof. intros. unfold Q_CongA_Null. split. auto. intros. assert(HH:=l11_21_a A B C A0 B0 C0 H1). apply HH. apply (ang_conga a); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid