proposition: Lemma diff_of_squares : forall O E E' A B A2 B2 A2MB2 APB AMB F, Prod O E E' A A A2 -> Prod O E E' B B B2 -> Diff O E E' A2 B2 A2MB2 -> Sum O E E' A B APB -> Diff O E E' A B AMB -> Prod O E E' APB AMB F -> A2MB2 = F.
proof: Proof. intros O E E' A B A2 B2 A2MB2 APB AMB F HA2 HB2 HA2MB2 HAPB HAMB HF. assert (HNC : ~ Col O E E') by (apply diff_ar2 in HA2MB2; unfold Ar2 in *; spliter; Col). assert (HColA : Col O E A) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColB : Col O E B) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColAMB : Col O E AMB) by (unfold Prod, Ar2 in *; spliter; Col). destruct (prod_exists O E E' HNC A AMB) as [F1 HF1]; Col. assert (HColF1 : Col O E F1) by (unfold Prod, Ar2 in *; spliter; Col). destruct (prod_exists O E E' HNC B AMB) as [F2 HF2]; Col. assert (HColF2 : Col O E F2) by (unfold Prod, Ar2 in *; spliter; Col). destruct (sum_exists O E E' HNC F1 F2) as [F' HF']; Col. assert (F = F'). { apply sum_uniqueness with O E E' F1 F2; auto. apply distr_r with A B AMB APB; auto. } treat_equalities; destruct (prod_exists O E E' HNC A B) as [AB HAB]; Col. assert (HColA2 : Col O E A2) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColAB : Col O E AB) by (unfold Prod, Ar2 in *; spliter; Col). destruct (diff_exists O E E' A2 AB) as [A2MAB HA2MAB]; Col. assert (A2MAB = F1). { apply diff_uniqueness with O E E' A2 AB; auto. apply distr_l_diff with A A B AMB; auto. } destruct (prod_exists O E E' HNC B A) as [BA HBA]; Col. assert (HColB2 : Col O E B2) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColBA : Col O E BA) by (unfold Prod, Ar2 in *; spliter; Col). destruct (diff_exists O E E' BA B2) as [BAMB2 HBAMB2]; Col. assert (BAMB2 = F2). { apply diff_uniqueness with O E E' BA B2; auto. apply distr_l_diff with B A B AMB; auto. } assert (AB = BA). { apply prod_uniqueness with O E E' A B; auto. apply prod_comm; auto. } treat_equalities; apply diff_uniqueness with O E E' A2 B2; auto. apply sum_diff_diff_b with AB BAMB2 A2MAB; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum