proposition: Lemma triangular_equality_equiv : (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)) <-> (forall O E E' A B C AB BC AC, O<>E -> 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. split. intros. assert(HH:= H O E A H0). apply (HH E' B C); auto. intros. assert(HH:= H O E E' A B C AB BC AC H0 H1 H2 H3 H4). assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order