proposition: Lemma length_eq_or_opp : forall O E E' A B L1 L2, Length O E E' A B L1 -> Diff O E E' A B L2 -> L1 = L2 \/ Opp O E E' L1 L2.
proof: Proof. intros O E E' A B L1 L2 HL1 HL2. assert (HNC : ~ Col O E E') by (apply diff_ar2 in HL2; unfold Ar2 in *; spliter; Col). assert (HColA : Col O E A) by (apply diff_ar2 in HL2; unfold Ar2 in *; spliter; Col). assert (HColB : Col O E B) by (apply diff_ar2 in HL2; unfold Ar2 in *; spliter; Col). elim (col_2_le_or_ge O E E' A B); auto; intro HLe; [right|left; apply l16_9_1 with O E E' A B; auto; left; auto]. apply diff_opp with B A; auto. destruct (diff_exists O E E' B A) as [D HD]; Col. assert (L1 = D) by (apply l16_9_1 with O E E' B A; auto; left; apply length_sym; auto). treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths