proposition: Lemma l16_9_2 : forall O E E' X Y XY XMY XY2 XMY2, Col O E X -> Col O E Y -> Is_length O E E' X Y XY -> Diff O E E' X Y XMY -> Prod O E E' XY XY XY2 -> Prod O E E' XMY XMY XMY2 -> XY2 = XMY2.
proof: Proof. intros O E E' X Y XY XMY XY2 XMY2 HCol1 HCol2 HXY HXMY HXY2 HXMY2. assert (HNC : ~ Col O E E') by (apply diff_ar2 in HXMY; unfold Ar2 in *; spliter; Col). assert (H:= HXY); elim H; clear H; intro HXY'; [|spliter; assert_diffs; intuition]. elim (length_eq_or_opp O E E' X Y XY XMY); auto; intro HOpp1; treat_equalities; apply prod_uniqueness with O E E' XY XY; auto. destruct (opp_exists O E E' HNC E) as [ME HOpp2]; Col. apply prod_assoc1 with XMY ME XMY; auto; [|apply prod_comm]; apply opp_prod;auto; apply opp_comm; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths