# Library HighSchoolGeometry.composee_dilatations

Require Export dilatations.
Set Implicit Arguments.
Unset Strict Implicit.

Lemma compo_transl :
A A' A1 I J K L : PO,
A1 = translation I J A
A' = translation K L A1 vec A A' = add_PP (vec I J) (vec K L).
intros A A' A1 I J K L H H0; try assumption.
cut (vec K L = vec A1 A'); intros.
cut (vec I J = vec A A1); intros.
rewrite H1; rewrite H2; Ringvec.
rewrite (translation_vecteur (I:=I) (J:=J) (A:=A) (A':=A1)); auto.
apply translation_vecteur; auto.
Qed.

Lemma composition_translation :
A A' A1 I J K L : PO,
A1 = translation I J A
A' = translation K L A1
ex
(fun M : PO
vec I M = add_PP (vec I J) (vec K L) :>PP A' = translation I M A).
intros A A' A1 I J K L H H0; try assumption.
elim
existence_representant_som_vecteur with (A := I) (B := J) (C := K) (D := L);
intros M H1; try clear existence_representant_som_vecteur;
try exact H1.
M.
split; [ try assumption | idtac ].
apply rec_translation_vecteur.
rewrite H1.
symmetry in |- *; apply compo_transl with A1; auto.
Qed.

Lemma compo_homothetie_I :
(k k' : R) (I A A' A1 : PO),
A1 = homothetie k I A :>PO
A' = homothetie k' I A1 :>PO A' = homothetie (k' × k) I A.
intros k k' I A A' A1 H H0; try assumption.
cut (vec I A' = mult_PP (k' × k) (vec I A)); intros.
apply vecteur_homothetie; auto.
rewrite <- mult_mult_vec.
rewrite <- (homothetie_vecteur (k:=k) (I:=I) (A:=A) (A':=A1)); auto.
apply homothetie_vecteur; auto.
Qed.

Lemma compo_homothetie_IJ :
(k k' : R) (I J A A' A1 : PO),
A1 = homothetie k I A :>PO
A' = homothetie k' J A1
cons 1 A' =
add_PP (add_PP (cons (k' × k) A) (cons (k' × (1 + - k)) I))
(cons (1 + - k') J) :>PP.
unfold vec, homothetie in |- *; intros.
rewrite H0; rewrite H.
rewrite (distrib_mult_cons k (1 + - k) k' A I).
replace (k + (1 + - k)) with 1; try ring; auto.
rewrite def_mult_PP.
replace (k' × 1) with k'; try ring; auto.
replace (k' + (1 + - k')) with 1; try ring; auto.
replace (k' + (1 + - k')) with 1; try ring; try discrR.
replace (k + (1 + - k)) with 1; try ring; try discrR.
Qed.

Lemma compo_homothetie_IJ_1 :
(k k' : R) (I J A A' A1 K : PO),
k' × k = 1
A1 = homothetie k I A :>PO
A' = homothetie k' J A1 :>PO
vec I K = mult_PP (1 + - k') (vec I J) :>PP A' = translation I K A.
intros.
cut (vec A A' = mult_PP (1 + - k') (vec I J)); intros.
apply rec_translation_vecteur; auto.
rewrite H3; rewrite H2; auto.
cut
(cons 1 A' =
add_PP (add_PP (cons (k' × k) A) (cons (k' × (1 + - k)) I))
(cons (1 + - k') J)); intros.
unfold vec in |- ×.
rewrite H3; auto.
replace (k' × (1 + - k)) with (- (k' × k) + k'); try ring; try ring; auto.
rewrite H; auto.
RingPP.
apply compo_homothetie_IJ with A1; auto.
Qed.

Lemma compo_homothetie_IJ_1_exists :
(k : R) (I J : PO),
k 0
K : PO,
( A A' A1 : PO,
A1 = homothetie k I A
A' = homothetie (/ k) J A1 :>PO A' = translation I K A).
intros.
elim
existence_representant_mult_vecteur
with (A := I) (B := I) (C := J) (k := 1 + - / k);
intros K H3; try clear existence_representant_mult_vecteur.
K; intros.
apply compo_homothetie_IJ_1 with (2 := H0) (3 := H1); auto with ×.
Qed.

Lemma compo_homothetie_IJ_non1 :
(k k' : R) (I J A A' A1 K : PO),
k' × k 1
A1 = homothetie k I A :>PO
A' = homothetie k' J A1 :>PO
K = barycentre (cons (k' × (1 + - k)) I) (cons (1 + - k') J) :>PO
A' = homothetie (k' × k) K A.
intros; unfold homothetie in |- ×.
cut (A' = barycentre (cons (k' × k) A) (cons (1 + - (k' × k)) K)); intros.
rewrite H3; auto.
elim
cons_inj
with
(a := 1)
(b := k' × k + (1 + - (k' × k)))
(A := A')
(B := barycentre (cons (k' × k) A) (cons (1 + - (k' × k)) K));
intros; auto with ×.
rewrite <- add_PP_barycentre; auto with real.
rewrite H2.
RReplace (1 + - (k' × k)) (k' × (1 + - k) + (1 + - k')).
rewrite <- add_PP_barycentre; auto with real.
apply compo_homothetie_IJ with A1; auto.
RReplace (k' × (1 + - k) + (1 + - k')) (1 + - (k' × k)).
auto with real.
RReplace (k' × k + (1 + - (k' × k))) 1.
auto with real.
Qed.

Lemma compo_homothetie_IJ_non1_exists :
(k k' : R) (I J : PO),
k' × k 1
K : PO,
( A A' A1 : PO,
A1 = homothetie k I A
A' = homothetie k' J A1 :>PO A' = homothetie (k' × k) K A :>PO).
intros.
(barycentre (cons (k' × (1 + - k)) I) (cons (1 + - k') J)); intros.
apply compo_homothetie_IJ_non1 with (2 := H0) (3 := H1); auto.
Qed.

Lemma composee_homothetie_translation :
(k : R) (A A' B B' B1 I J : PO),
k 1
k 0
B1 = homothetie k I B :>PO
B' = translation A A' B1 :>PO
J =
barycentre (cons 1 A')
(cons (-1 + (1 + - k)) (barycentre (cons (-1) A) (cons (1 + - k) I))) :>PO
B' = homothetie k J B.
unfold translation, homothetie in |- *;
intros k A A' B B' B1 I J H H0 H1 H2 H30.
elim
cons_inj
with
(a := 1)
(b := 1)
(A := B')
(B := barycentre (cons k B)
(cons (1 + - k)
(barycentre (cons 1 A')
(cons (-1 + (1 + - k))
(barycentre (cons (-1) A) (cons (1 + - k) I))))));
intros; auto with ×.
rewrite H4; rewrite H30; auto.
rewrite H2.
pattern 1 at 1 in |- ×.
replace 1 with (-1 + 2); [ idtac | try ring ].
pattern 1 at 3 in |- ×.
replace 1 with (k + (1 + - k)); [ idtac | try ring ].
rewrite H1.
pattern 1 at 4 in |- ×.
replace 1 with (k + (1 + - k)); [ idtac | try ring ].
pattern (1 + - k) at 2 in |- ×.
replace (1 + - k) with (1 + (-1 + (1 + - k))); [ idtac | try ring ].
RingPP.
replace (-1 + (1 + - k)) with (- k); try ring; auto with ×.
replace (1 + (-1 + (1 + - k))) with (1 + - k); try ring; auto with ×.
replace (k + (1 + - k)) with 1; try ring; auto with ×.
replace (k + (1 + - k)) with 1; try ring; auto with ×.
discrR.
replace (-1 + 2) with 1; try ring; auto with ×.
Qed.

Lemma composee_homothetie_translation_exists :
(k : R) (I A A' : PO),
k 1 :>R
k 0 :>R
J : PO,
( B B' B1 : PO,
B1 = homothetie k I B :>PO
B' = translation A A' B1 :>PO B' = homothetie k J B :>PO).
intros.

(barycentre (cons 1 A')
(cons (-1 + (1 + - k)) (barycentre (cons (-1) A) (cons (1 + - k) I))));
intros.
apply composee_homothetie_translation with (4 := H2) (3 := H1); auto.
Qed.

Lemma composee_translation_homothetie :
(k : R) (A A' B B' B1 I J : PO),
k 1
k 0
B1 = translation A A' B :>PO
B' = homothetie k I B1 :>PO
J =
barycentre (cons (- k) A)
(cons (k + (1 + - k)) (barycentre (cons k A') (cons (1 + - k) I))) :>PO
B' = homothetie k J B.
unfold translation, homothetie in |- *;
intros k A A' B B' B1 I J H H0 H1 H2 H30.
elim
cons_inj
with
(a := 1)
(b := 1)
(A := B')
(B := barycentre (cons k B)
(cons (1 + - k)
(barycentre (cons (- k) A)
(cons (k + (1 + - k))
(barycentre (cons k A') (cons (1 + - k) I))))));
intros; auto with ×.
rewrite H4; rewrite H30; auto.
rewrite H2.
cut (cons k B1 = add_PP (cons (- k) A) (add_PP (cons k A') (cons k B)));
intros.
pattern 1 at 1 in |- ×.
replace 1 with (k + (1 + - k)); [ idtac | try ring ].
rewrite H3.
pattern 1 at 2 in |- ×.
replace 1 with (k + (1 + - k)); [ idtac | try ring ].
pattern (1 + - k) at 2 in |- ×.
replace (1 + - k) with (- k + (k + (1 + - k))); [ idtac | try ring ].
RingPP.
replace (k + (1 + - k)) with 1; try ring; auto with ×.
replace (- k + (k + (1 + - k))) with (1 + - k); try ring; auto with ×.
replace (k + (1 + - k)) with 1; try ring; auto with ×.
replace (k + (1 + - k)) with 1; try ring; auto with ×.
apply mult_PP_regulier with (/ k); auto with real.
replace
(mult_PP (/ k) (add_PP (cons (- k) A) (add_PP (cons k A') (cons k B)))) with
replace (mult_PP (/ k) (cons k B1)) with (cons 1 B1).
rewrite H1.
pattern 1 at 1 in |- ×.
replace 1 with (-1 + 2); [ idtac | try ring ].
rewrite <- add_PP_barycentre; auto with real.
rewrite <- add_PP_barycentre; auto with real.
discrR.
Fieldvec k.
Fieldvec k.
Qed.

Lemma composee_translation_homothetie_exists :
(k : R) (I A A' : PO),
k 1 :>R
k 0 :>R
J : PO,
( B B' B1 : PO,
B1 = translation A A' B :>PO
B' = homothetie k I B1 :>PO B' = homothetie k J B :>PO).
intros.

(barycentre (cons (- k) A)
(cons (k + (1 + - k)) (barycentre (cons k A') (cons (1 + - k) I))));
intros.
apply composee_translation_homothetie with (4 := H2) (3 := H1); auto.
Qed.