proposition: Lemma eq_squares_eq_or_opp : forall O E E' A B A2, Prod O E E' A A A2 -> Prod O E E' B B A2 -> A = B \/ Opp O E E' A B.
proof: Proof. intros O E E' A B A2 HA2 HB2. assert (HNC : ~ Col O E E') by (unfold Prod, Ar2 in *; spliter; Col). assert (HColA : Col O E A) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColA2 : Col O E A2) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColB : Col O E B) by (unfold Prod, Ar2 in *; spliter; Col). destruct (diff_exists O E E' A2 A2) as [O' HA2MA2]; Col. assert (O = O') by (apply diff_uniqueness with O E E' A2 A2; auto; apply diff_null; Col). destruct (sum_exists O E E' HNC A B) as [APB HAPB]; Col. assert (HColAPB : Col O E APB) by (unfold Sum, Ar2 in *; spliter; Col). destruct (diff_exists O E E' A B) as [AMB HAMB]; Col; treat_equalities. assert (HColAMB : Col O E AMB) by (apply diff_sum in HAMB; unfold Sum, Ar2 in *; spliter; Col). destruct (prod_exists O E E' HNC APB AMB) as [O' H]; Col. assert (O = O') by (apply diff_of_squares with O E E' A B A2 A2 APB AMB; auto). treat_equalities; apply prod_null in H; induction H; treat_equalities; [right; apply sum_opp|left; apply diff_null_eq with AMB E E']; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum