proposition: Lemma l16_9_1 : forall O E E' X Y XY XMY, Col O E X -> Col O E Y -> Is_length O E E' X Y XY -> LeP O E E' Y X -> Diff O E E' X Y XMY -> XY = XMY.
proof: Proof. intros O E E' X Y XY XMY HCol1 HCol2 HXY HLe1 HXMY. assert (HNC : ~ Col O E E') by (apply diff_ar2 in HXMY; unfold Ar2 in *; spliter; Col). assert (HOE : O <> E) by (assert_diffs; auto). assert (HCol3 : Col O E XMY). { unfold Diff, Opp, Sum, Ar2 in *; destruct HXMY as [MB [H1 [H2 [H3 H4]]]]; spliter; Col. } assert (HCong1 := HXMY); apply diff_sum in HCong1; apply l15_3 in HCong1. elim HXY; clear HXY; intro HXY; [|spliter; intuition]. destruct HXY as [H [HCol4 [HLe2 HCong2]]]. elim (l7_20 O XY XMY); [auto|intro HMid; clear H|ColR|apply cong_transitivity with X Y; Cong]. elim HLe1; clear HLe1; intro HLt1; [clear HCong1|treat_equalities; auto]. elim HLe2; clear HLe2; intro HLt2; [clear HCong2|treat_equalities; auto]. exfalso; apply not_pos_and_neg with O E XMY; split; [apply lt_diff_ps with E' X Y; auto|]. apply pos_opp_neg with E' XY; [apply ltP_pos with E'; auto|]. apply midpoint_opp; repeat (Col; split). Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths