proposition: Lemma not_triangular_equality1 : forall O E A , O<>E -> ~ (forall E' B C AB BC AC, Bet A B C -> Length O E E' A B AB -> Length O E E' B C BC -> Length O E E' A C AC -> Sum O E E' AB BC AC).
proof: Proof. intros. intro. assert(HH:=(H0 E A A O O O)). assert(Bet A A A); Between. assert(Length O E E A A O). apply(length_id_2); auto. assert(HHH:= (HH H1 H2 H2 H2)). unfold Sum in HHH. spliter. ex_and H4 X. ex_and H5 Y. unfold Ar2 in H3. spliter. apply H3. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order