proposition: Lemma length_not_neg : forall O E E' A B AB, Length O E E' A B AB -> ~Ng O E AB.
proof: Proof. intros. intro. assert(HH:= length_cong O E E' A B AB H). apply length_pos_or_null in H. induction H. { apply pos_not_neg in H. contradiction. } { unfold Ng in H0. spliter. subst B. treat_equalities. tauto. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order