proposition: Lemma characterization_of_congruence : forall O E E' S U1 U2 A AX AY B BX BY C CX CY D DX DY AXMBX AXMBX2 AYMBY AYMBY2 AB2 CXMDX CXMDX2 CYMDY CYMDY2 CD2, Cd O E S U1 U2 A AX AY -> Cd O E S U1 U2 B BX BY -> Cd O E S U1 U2 C CX CY -> Cd O E S U1 U2 D DX DY -> Diff O E E' AX BX AXMBX -> Prod O E E' AXMBX AXMBX AXMBX2 -> Diff O E E' AY BY AYMBY -> Prod O E E' AYMBY AYMBY AYMBY2 -> Sum O E E' AXMBX2 AYMBY2 AB2 -> Diff O E E' CX DX CXMDX -> Prod O E E' CXMDX CXMDX CXMDX2 -> Diff O E E' CY DY CYMDY -> Prod O E E' CYMDY CYMDY CYMDY2 -> Sum O E E' CXMDX2 CYMDY2 CD2 -> (Cong A B C D <-> AB2 = CD2).
proof: Proof. intros O E E' S U1 U2 A AX AY B BX BY C CX CY D DX DY. intros AXMBX AXMBX2 AYMBY AYMBY2 AB2' CXMDX CXMDX2 CYMDY CYMDY2 CD2'. intros HCdA HCdB HCdC HCdD HAXMBX HAXMBX2 HAYMBY HAYMBY2 HAB2. intros HCXMDX HCXMDX2 HCYMDY HCYMDY2 HCD2. assert (HNC : ~ Col O E E') by (apply diff_ar2 in HAXMBX; unfold Ar2 in *; spliter; Col). destruct (is_length_exists O E E' A B) as [AB HLengthAB]; Col. assert (HColAB : Col O E AB). { unfold Is_length, Length in *; induction HLengthAB; spliter; treat_equalities; Col. } destruct (prod_exists O E E' HNC AB AB) as [AB2 HLengthAB2]; Col. assert (AB2 = AB2'). { apply square_distance_formula with O E E' S U1 U2 A B AX AY BX BY AB AXMBX AYMBY AXMBX2 AYMBY2; auto. } treat_equalities; clear HAB2; clear HAYMBY2; clear HAYMBY; clear HAXMBX2; clear HAXMBX; clear HCdA; clear HCdB. destruct (is_length_exists O E E' C D) as [CD HLengthCD]; Col. assert (HColCD : Col O E CD). { unfold Is_length, Length in *; induction HLengthCD; spliter; treat_equalities; Col. } destruct (prod_exists O E E' HNC CD CD) as [CD2 HLengthCD2]; Col. assert (CD2 = CD2'). { apply square_distance_formula with O E E' S U1 U2 C D CX CY DX DY CD CXMDX CYMDY CXMDX2 CYMDY2; auto. } treat_equalities; clear HCD2; clear HCYMDY2; clear HCYMDY; clear HCXMDX2; clear HCXMDX; clear HCdC; clear HCdD. split; [intro HCong|intro; treat_equalities]. { assert (H : Cong O AB O CD). { unfold Is_length, Length in *; induction HLengthAB; [|spliter; treat_equalities; exfalso; apply HNC; Col]; induction HLengthCD; [|spliter; treat_equalities; exfalso; apply HNC; Col]. spliter; apply cong_transitivity with A B; trivial. apply cong_transitivity with C D; Cong. } clear HLengthAB; clear HLengthCD; clear HCong; rename H into HCong. assert (H : Col O AB CD) by ColR. elim (l7_20 O AB CD); Col; clear H; clear HCong; intro HMid; treat_equalities. { apply prod_uniqueness with O E E' AB AB; auto. } { assert (HOpp1 : Opp O E E' AB CD) by (apply midpoint_opp; unfold Ar2; auto; repeat (split; Col)). clear HMid; destruct (opp_exists O E E' HNC E) as [ME HOpp2]; Col. assert (Prod O E E' AB ME CD) by (apply opp_prod; auto). assert (HXMY2' : Prod O E E' CD CD AB2). { apply prod_assoc1 with AB ME AB; auto. apply prod_assoc2 with ME AB E; try apply prod_1_l; Col; apply prod_comm; auto. apply opp_prod; auto; apply opp_comm; auto. } apply prod_uniqueness with O E E' CD CD; auto. } } { elim HLengthAB; clear HLengthAB; intro HLengthAB; [|spliter; treat_equalities; exfalso; apply HNC; Col]. elim HLengthCD; clear HLengthCD; intro HLengthCD; [|spliter; treat_equalities; exfalso; apply HNC; Col]. elim (eq_squares_eq_or_opp O E E' AB CD AB2); auto; intro HOpp; treat_equalities; [apply length_eq_cong_1 with O E E' AB; auto|]. unfold Length, LeP, LtP in *; spliter; apply opp_midpoint in HOpp. unfold Midpoint in *; spliter. apply cong_transitivity with O CD; trivial. apply cong_transitivity with O AB; Cong. } Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths