Require Export homothetie_plane.
Set Implicit Arguments.
Unset Strict Implicit.
Parameter similitude : PO → R → R → PO → PO.

Axiom
  similitude_def :
    ∀ (I A B : PO) (k a : R),
    k > 0 →
    I ≠ A →
    B = similitude I k a A →
    distance I B = k × distance I A ∧
    image_angle a = cons_AV (vec I A) (vec I B).

Axiom
  similitude_def_centre :
    ∀ (I : PO) (k a : R), k > 0 → I = similitude I k a I.

Axiom
  similitude_def2 :
    ∀ (I A B : PO) (k a : R),
    k > 0 →
    I ≠ A →
    distance I B = k × distance I A →
    image_angle a = cons_AV (vec I A) (vec I B) → B = similitude I k a A.

Lemma composee_rotation_homothetie_pos :
 ∀ (I M M' M1 : PO) (k a : R),
 k > 0 →
 M1 = rotation I a M → M' = homothetie k I M1 → M' = similitude I k a M.
intros I M M' M1 k a H; try assumption.
discrimine I M.
rewrite <- similitude_def_centre; auto; rewrite <- rotation_def_centre;
 intros.
rewrite H2; rewrite H1; rewrite <- homothetie_centre; auto.
intros.
elim rotation_def with (I := I) (A := M) (B := M1) (a := a);
 [ intros | auto | auto ].
cut (distance I M' = Rabs k × distance I M1); intros.
2: apply distance_homothetie with I; auto with geo.
apply similitude_def2; auto.
rewrite H5; rewrite H3; rewrite Rabs_right; auto.
fourier.
rewrite H4; auto.
cut (vec I M' = mult_PP k (vec I M1)); intros.
symmetry in |- *;
 rewrite
  (angle_produit_positif_r (k:=k) (A:=I) (B:=M1) (C:=M') (D:=I) (E:=M))
  ; auto.
apply image_distinct_centre with (2 := H1); auto.
apply homothetie_vecteur; auto.
Qed.

Lemma composee_homothetie_pos_rotation :
 ∀ (I M M' M1 : PO) (k a : R),
 k > 0 →
 M1 = homothetie k I M → M' = rotation I a M1 → M' = similitude I k a M.
intros I M M' M1 k a H; try assumption.
discrimine I M.
rewrite <- similitude_def_centre; auto; rewrite <- homothetie_centre; intros.
rewrite H2; rewrite H1; rewrite <- rotation_def_centre; auto.
intros.
cut (vec I M1 = mult_PP k (vec I M)); intros.
cut (distance I M1 = Rabs k × distance I M); intros.
2: apply distance_homothetie with I; auto with geo.
cut (I ≠ M1); intros.
cut (I ≠ M'); intros.
elim rotation_def with (I := I) (A := M1) (B := M') (a := a);
 [ intros | auto | auto ].
apply similitude_def2; auto.
rewrite <- H7; rewrite H4; rewrite Rabs_right; auto.
fourier.
rewrite H8.
apply permute_angles; auto.
rewrite (angle_produit_positif_r (k:=k) (A:=I) (B:=M) (C:=M1) (D:=I) (E:=M'));
 auto.
apply image_distinct_centre with (2 := H2); auto with geo.
apply distinct_produit_vecteur with (3 := H3); auto.
auto with real.
apply homothetie_vecteur; auto.
Qed.

Lemma existence_similitude_Ika :
 ∀ (I M : PO) (k a : R),
 k > 0 → ∃ M' : PO, M' = similitude I k a M.
intros.
elim existence_rotation_Ia with (I := I) (M := M) (a := a); intros M1; intros.
elim existence_homothetique with (k := k) (I := I) (A := M1); intros M' H1;
 try clear existence_homothetique; try exact H1.
∃ M'.
apply composee_rotation_homothetie_pos with M1; auto.
Qed.

Lemma similitude_rapport_un :
 ∀ (I A : PO) (a : R), rotation I a A = similitude I 1 a A.
intros.
discrimine I A.
rewrite <- rotation_def_centre; rewrite <- similitude_def_centre; auto.
fourier.
elim existence_rotation_Ia with (I := I) (M := A) (a := a); intros B; intros.
cut (B = homothetie 1 I B); intros.
2: apply homothetie_identite.
rewrite <- H0.
apply composee_rotation_homothetie_pos with B; auto.
fourier.
Qed.

Lemma similitude_angle_nul :
 ∀ (I A : PO) (k : R), k > 0 → homothetie k I A = similitude I k 0 A.
intros.
discrimine I A.
rewrite <- homothetie_centre; rewrite <- similitude_def_centre; auto.
cut (A = rotation I 0 A); intros.
2: apply rotation_angle_nul.
elim existence_homothetique with (k := k) (I := I) (A := A); intros M';
 intros.
rewrite <- H2.
apply composee_rotation_homothetie_pos with A; auto.
Qed.

Lemma similitude_identite : ∀ I A : PO, A = similitude I 1 0 A.
intros.
rewrite <- similitude_rapport_un.
rewrite <- rotation_angle_nul; auto.
Qed.

Lemma image_sim_distinct_centre :
 ∀ (I A B : PO) (k a : R),
 I ≠ A → k > 0 → B = similitude I k a A → I ≠ B.
intros.
elim similitude_def with (I := I) (A := A) (B := B) (k := k) (a := a);
 [ intros | auto | auto | auto ].
apply dist_non_nulle.
rewrite H2.
apply prod_neq_R0; auto with geo.
auto with real.
Qed.

Lemma similitude_decomposition :
 ∀ (I M M' : PO) (k a : R),
 k > 0 →
 M' = similitude I k a M →
 ∃ M1 : PO, M1 = rotation I a M ∧ M' = homothetie k I M1.
intros.
elim existence_rotation_Ia with (I := I) (M := M) (a := a); intros M1; intros.
∃ M1.
split; [ try assumption | idtac ].
discrimine I M.
rewrite <- H2 in H1; rewrite <- H2 in H0.
rewrite <- similitude_def_centre in H0; auto;
 rewrite <- rotation_def_centre in H1.
rewrite <- H2; rewrite H0; rewrite H1; auto with geo.
cut (I ≠ M1); intros.
cut (I ≠ M'); intros.
apply vecteur_homothetie.
elim similitude_def with (I := I) (A := M) (B := M') (k := k) (a := a);
 [ intros | auto | auto | auto ].
elim rotation_def with (I := I) (A := M) (B := M1) (a := a);
 [ intros | auto | auto ].
apply alignes_distance_positif_colineaire; auto.
replace (cons_AV (vec I M1) (vec I M')) with
 (plus (cons_AV (vec I M) (vec I M')) (opp (cons_AV (vec I M) (vec I M1)))).
rewrite def_opp; auto.
rewrite <- (mes_oppx (A:=I) (B:=M) (C:=I) (D:=M1) (x:=a)); auto.
rewrite <- H6.
repeat rewrite <- add_mes_compatible.
replace (a + - a) with 0; auto.
ring.
apply Chasles_diff; auto.
rewrite <- H7; auto.
apply image_sim_distinct_centre with (3 := H0); auto.
apply image_distinct_centre with (2 := H1); auto.
Qed.

Lemma rotation_homothetie_pos_I_commutent :
 ∀ (I M M1 M2 : PO) (k a : R),
 k > 0 →
 M1 = homothetie k I M →
 M2 = rotation I a M → homothetie k I M2 = rotation I a M1.
intros.
elim existence_rotation_Ia with (I := I) (M := M1) (a := a); intros N; intros.
elim existence_homothetique with (k := k) (I := I) (A := M2); intros N';
 intros.
rewrite <- H3; rewrite <- H2.
rewrite
 (composee_rotation_homothetie_pos (I:=I) (M:=M) (M':=N') (M1:=M2) (k:=k)
    (a:=a)); auto.
rewrite
 (composee_homothetie_pos_rotation (I:=I) (M:=M) (M':=N) (M1:=M1) (k:=k)
    (a:=a)); auto.
Qed.

Lemma similitudes_meme_centre_commutent :
 ∀ (I M M1 M2 : PO) (k m a b : R),
 k > 0 →
 m > 0 →
 M1 = similitude I k a M →
 M2 = similitude I m b M → similitude I k a M2 = similitude I m b M1.
intros I M M1 M2 k m a b H H0; try assumption.
discrimine I M.
repeat (rewrite <- similitude_def_centre; auto).
intros H2 H3; try assumption.
rewrite H2; rewrite H3.
repeat (rewrite <- similitude_def_centre; auto).
intros H2 H3; try assumption.
elim existence_similitude_Ika with (I := I) (M := M1) (k := m) (a := b);
 [ intros N H4 | auto ].
elim existence_similitude_Ika with (I := I) (M := M2) (k := k) (a := a);
 [ intros M' H5 | auto ].
rewrite <- H5.
cut (I ≠ M1); intros.
2: apply image_sim_distinct_centre with (3 := H2); auto.
cut (I ≠ M2); intros.
2: apply image_sim_distinct_centre with (3 := H3); auto.
cut (I ≠ M'); intros.
2: apply image_sim_distinct_centre with (3 := H5); auto.
cut (I ≠ N); intros.
2: apply image_sim_distinct_centre with (3 := H4); auto.
elim similitude_def with (I := I) (A := M2) (B := M') (k := k) (a := a);
 [ intros | auto | auto | auto ].
elim similitude_def with (I := I) (A := M1) (B := N) (k := m) (a := b);
 [ intros | auto | auto | auto ].
elim similitude_def with (I := I) (A := M) (B := M2) (k := m) (a := b);
 [ intros | auto | auto | auto ].
elim similitude_def with (I := I) (A := M) (B := M1) (k := k) (a := a);
 [ intros | auto | auto | auto ].
apply similitude_def2; auto.
rewrite H16; rewrite H10; rewrite H14; ring.
replace (cons_AV (vec I M1) (vec I M')) with
 (plus
    (plus (cons_AV (vec I M) (vec I M2)) (opp (cons_AV (vec I M) (vec I M1))))
    (cons_AV (vec I M2) (vec I M'))).
rewrite def_opp; auto.
rewrite <- (mes_oppx (A:=I) (B:=M) (C:=I) (D:=M1) (x:=a)); auto.
rewrite <- H15; rewrite <- H11.
repeat rewrite <- add_mes_compatible.
replace (b + - a + a) with b; auto.
ring.
rewrite Chasles_diff; auto.
rewrite Chasles; auto.
Qed.

Lemma homothetie_neg :
 ∀ (I M M' : PO) (k : R),
 k < 0 → M' = homothetie k I M → M' = similitude I (- k) pi M.
intros I M M' k H; try assumption.
discrimine I M.
rewrite <- homothetie_centre.
rewrite <- similitude_def_centre; auto.
fourier.
intros.
cut (vec I M' = mult_PP k (vec I M)); intros.
cut (distance I M' = Rabs k × distance I M); intros.
2: apply distance_homothetie with I; auto with geo.
2: apply homothetie_vecteur; auto.
cut (I ≠ M'); intros.
apply similitude_def2; auto.
fourier.
rewrite <- Rabs_left; auto.
rewrite (angle_produit_negatif_r (k:=k) (A:=I) (B:=M) (C:=M') (D:=I) (E:=M));
 auto.
rewrite <- angle_nul; auto.
repeat rewrite <- add_mes_compatible.
replace (0 + pi) with pi; auto.
ring.
apply distinct_produit_vecteur with (3 := H2); auto.
auto with real.
Qed.

Lemma homothetie_neg2 :
 ∀ (I M : PO) (k : R),
 k < 0 → homothetie k I M = similitude I (- k) pi M.
intros.
elim existence_homothetique with (k := k) (I := I) (A := M); intros M';
 intros.
rewrite <- H0.
apply homothetie_neg; auto.
Qed.

Lemma rotation_homothetie_I_commutent :
 ∀ (I M M1 M2 : PO) (k a : R),
 k ≠ 0 →
 M1 = homothetie k I M →
 M2 = rotation I a M → homothetie k I M2 = rotation I a M1.
intros I M M1 M2 k a H; try assumption.
repeat rewrite similitude_rapport_un.
elim Rtotal_order with (r1 := k) (r2 := 0);
 [ intros H4; try clear total_order
 | intros H4;
    (elim H4;
      [ intros H5; try clear H4 total_order
      | intros H5; try clear H4 total_order; try exact H5 ]) ].
repeat (rewrite homothetie_neg2; auto).
intros.
apply similitudes_meme_centre_commutent with (3 := H0) (4 := H1); auto.
auto with real.
fourier.
absurd (k = 0); auto with real.
repeat (rewrite similitude_angle_nul; auto).
intros.
apply similitudes_meme_centre_commutent with (3 := H0) (4 := H1); auto.
fourier.
Qed.

Lemma similitude_conserve_angle :
 ∀ (I A B C A' B' C' : PO) (k a : R),
 k > 0 →
 A ≠ B →
 A ≠ C →
 A' = similitude I k a A →
 B' = similitude I k a B →
 C' = similitude I k a C →
 cons_AV (vec A B) (vec A C) = cons_AV (vec A' B') (vec A' C').
intros.
elim
 similitude_decomposition with (I := I) (M := A) (M' := A') (k := k) (a := a);
 [ intros A1 H7; elim H7; intros H8 H9; try clear H7 | auto | auto ].
elim
 similitude_decomposition with (I := I) (M := B) (M' := B') (k := k) (a := a);
 [ intros B1 H7; elim H7; intros H10 H11; try clear H7; try exact H11
 | auto
 | auto ].
elim
 similitude_decomposition with (I := I) (M := C) (M' := C') (k := k) (a := a);
 [ intros C1 H7; elim H7; intros H12 H13; try clear H7; try exact H13
 | auto
 | auto ].
cut (A1 ≠ B1); intros.
cut (A1 ≠ C1); intros.
cut (cons_AV (vec A B) (vec A C) = cons_AV (vec A1 B1) (vec A1 C1)); intros.
rewrite H7.
apply
 (homothetie_conserve_angle (I:=I) (A:=A1) (B:=B1) (C:=C1) (A':=A') (B':=B')
    (C':=C') (k:=k)); auto with real.
apply
 (rotation_conserve_angle (I:=I) (A:=A) (B:=B) (C:=C) (A':=A1) (B':=B1)
    (C':=C1) (a:=a)); auto.
apply image_bipoint_distinct with (2 := H8) (3 := H12); auto.
apply image_bipoint_distinct with (2 := H8) (3 := H10); auto.
Qed.

Lemma distance_similitude :
 ∀ (k a : R) (I A B A' B' : PO),
 k > 0 →
 A' = similitude I k a A →
 B' = similitude I k a B → distance A' B' = k × distance A B.
intros.
elim
 similitude_decomposition with (I := I) (M := A) (M' := A') (k := k) (a := a);
 [ intros A1 H7; elim H7; intros H8 H9; try clear H7 | auto | auto ].
elim
 similitude_decomposition with (I := I) (M := B) (M' := B') (k := k) (a := a);
 [ intros B1 H7; elim H7; intros H10 H11; try clear H7; try exact H11
 | auto
 | auto ].
cut (distance A1 B1 = distance A B); intros.
rewrite <- H2.
rewrite (distance_homothetie (k:=k) (I:=I) (A:=A1) (A':=A') (B:=B1) (B':=B'));
 auto.
rewrite Rabs_right; auto.
red in |- *; auto.
apply rotation_isometrie with (1 := H8) (2 := H10).
Qed.