# Library HighSchoolGeometry.metrique_triangle

Require Export euclidien_classiques.
Require Export trigo.
Set Implicit Arguments.
Unset Strict Implicit.

Lemma produit_scalaire_Cosinus :
A B C : PO,
A B
A C
scalaire (vec A B) (vec A C) =
distance A B × (distance A C × Cos (cons_AV (vec A B) (vec A C))).
intros.
elim existence_representant_unitaire with (A := A) (B := B);
[ intros H2; try clear existence_representant_unitaire; try exact H2
| auto ].
elim existence_representant_unitaire with (A := A) (B := C);
[ intros H3; try clear existence_representant_unitaire; try exact H3
| auto ].
elim existence_ROND_AB with (A := A) (B := ); [ intros D H10 | auto ].
elim H10; intros.
elim H4; intros H6 H7; try clear H4; try exact H7.
rewrite angles_representants_unitaires; auto with geo.
pattern (vec A B) at 1 in |- ×.
rewrite distance_vecteur; auto.
pattern (vec A C) at 1 in |- ×.
rewrite distance_vecteur; auto.
rewrite <- H3; rewrite <- H2.
pattern (vec A ) at 1 in |- ×.
rewrite (coordonnees_Cos_Sin (O:=A) (I:=) (J:=D) (M:=)); auto.
replace
(mult_PP (distance A C)
(add_PP (mult_PP (Cos (cons_AV (vec A ) (vec A ))) (vec A ))
(mult_PP (Sin (cons_AV (vec A ) (vec A ))) (vec A D)))) with
(mult_PP (distance A C × Cos (cons_AV (vec A ) (vec A ))) (vec A ))
(mult_PP (distance A C × Sin (cons_AV (vec A ) (vec A ))) (vec A D))).
replace (mult_PP (distance A B) (vec A )) with
(add_PP (mult_PP (distance A B) (vec A )) (mult_PP 0 (vec A D))).
Simplscal.
replace (scalaire (vec A ) (vec A D)) with 0.
rewrite H6; ring.
symmetry in |- *; auto with geo.
Ringvec.
Ringvec.
elim def_representant_unitaire2 with (A := A) (B := C) (C := );
auto with geo; intros.
elim H5; auto with geo.
elim def_representant_unitaire2 with (A := A) (B := B) (C := ); auto;
intros.
elim H4; auto with geo.
Qed.

Lemma produit_scalaire_cosinus :
(A B C : PO) (a : R),
A B
A C
image_angle a = cons_AV (vec A B) (vec A C) →
scalaire (vec A B) (vec A C) = distance A B × (distance A C × cos a).
intros.
rewrite produit_scalaire_Cosinus; auto.
rewrite (egalite_cos_Cos (A:=A) (B:=B) (C:=C) (x:=a)); auto.
Qed.
Hint Resolve carre_scalaire_distance: geo.

Lemma triangle_rectangle_Cos :
(A B C : PO) (a : R),
A B
A C
orthogonal (vec B A) (vec B C) →
distance A B = distance A C × Cos (cons_AV (vec A B) (vec A C)).
intros.
cut
(scalaire (vec A B) (vec A C) =
distance A B × (distance A C × Cos (cons_AV (vec A B) (vec A C))));
intros.
2: apply produit_scalaire_Cosinus; auto.
apply Rmult_eq_reg_l with (distance A B); auto with geo.
rewrite <- H2.
rewrite (scalaire_avec_projete (A:=A) (B:=B) (C:=C) (H:=B)); auto with geo.
Qed.

Lemma triangle_rectangle_cos :
(A B C : PO) (a : R),
A B
A C
orthogonal (vec B A) (vec B C) →
image_angle a = cons_AV (vec A B) (vec A C) →
distance A B = distance A C × cos a.
intros.
rewrite (triangle_rectangle_Cos (A:=A) (B:=B) (C:=C)); auto.
rewrite (egalite_cos_Cos (A:=A) (B:=B) (C:=C) (x:=a)); auto.
Qed.

Lemma triangle_rectangle_absolu_cos :
(A B C : PO) (a : R),
A B
A C
orthogonal (vec B A) (vec B C) →
image_angle a = cons_AV (vec A B) (vec A C) →
distance A B = distance A C × Rabs (cos a).
intros.
cut (/ distance A C 0); intros; auto with geo.
cut (distance A B 0); intros; auto with geo.
cut (cos a 0); intros.
rewrite Rabs_right; auto with real.
apply triangle_rectangle_cos; auto.
replace (cos a) with (distance A B × / distance A C).
RReplace 0 (0 × / distance A C).
apply Rmult_ge_compat_r; auto.
rewrite (triangle_rectangle_cos (A:=A) (B:=B) (C:=C) (a:=a)); intros;
auto with geo.
field.
auto with geo.
apply Rinv_le_pos; auto with geo.
Qed.

Lemma orthogonal_distincts :
A B C : PO,
A BA Corthogonal (vec A B) (vec A C) → B C.
intros.
apply non_alignes_distincts2 with A; auto.
apply orthogonal_non_alignes; auto with geo.
Qed.

Lemma triangle_rectangle_direct_sinus :
(A B C : PO) (a : R),
A B
A C
B C
image_angle pisurdeux = cons_AV (vec B C) (vec B A) →
image_angle a = cons_AV (vec A B) (vec A C) →
distance C B = distance C A × sin a.
intros.
cut (image_angle (pisurdeux + - a) = cons_AV (vec C A) (vec C B)); intros.
rewrite sin_cos_pisurdeux_moins_x.
rewrite <- cos_paire.
rewrite <-
(triangle_rectangle_cos (A:=C) (B:=B) (C:=A) (a:=- (pisurdeux + - a)))
; auto with geo.
apply mes_oppx; auto.
replace (cons_AV (vec C A) (vec C B)) with
(plus (image_angle pi)
(opp (plus (cons_AV (vec A B) (vec A C)) (cons_AV (vec B C) (vec B A)))));
auto with geo.
rewrite opp_plus_plus_opp; auto.
rewrite <- H3; rewrite <- H2.
repeat rewrite <- mes_opp.
replace (pisurdeux + - a) with (pi + (- a + - pisurdeux)); auto.
unfold pi in |- *; ring.
Qed.

Lemma triangle_rectangle_indirect_sinus :
(A B C : PO) (a : R),
A B
A C
B C
image_angle (- pisurdeux) = cons_AV (vec B C) (vec B A) →
image_angle a = cons_AV (vec A B) (vec A C) →
distance C B = distance C A × - sin a.
intros A B C a H H0 H1 H2 H3; try assumption.
elim pisurdeux_plus_x with (x := a);
[ intros H5 H6; try clear pisurdeux_plus_x; try rewrite <- H5 ].
rewrite <- (triangle_rectangle_cos (A:=C) (B:=B) (C:=A) (a:=pisurdeux + a));
auto with geo.
cut (orthogonal (vec B A) (vec B C)); auto with geo.
apply pisurdeux_droit.
RReplace pisurdeux (- - pisurdeux).
apply mes_oppx; auto with geo.
RReplace (pisurdeux + a) (- - (pisurdeux + a)).
apply mes_oppx; auto with geo.
replace (cons_AV (vec C A) (vec C B)) with
(plus (image_angle pi)
(opp (plus (cons_AV (vec A B) (vec A C)) (cons_AV (vec B C) (vec B A)))));
auto with geo.
rewrite opp_plus_plus_opp; auto.
rewrite <- H3; rewrite <- H2.
repeat rewrite <- mes_opp.
rewrite <- (plus_angle_zero (image_angle (- (pisurdeux + a)))).
rewrite <- pi_plus_pi.
replace (- (pisurdeux + a) + deuxpi) with (pi + (- a + - - pisurdeux)); auto.
unfold deuxpi, pi in |- *; ring.
Qed.

Lemma triangle_rectangle_absolu_sinus :
(A B C : PO) (a : R),
A B
A C
B C
orthogonal (vec B A) (vec B C) →
image_angle a = cons_AV (vec A B) (vec A C) →
distance C B = distance C A × Rabs (sin a).
intros.
cut (/ distance C A 0); intros; auto with geo.
2: apply Rinv_le_pos; auto with geo.
cut (distance C B 0); intros; auto with geo.
elim orthogonal_pisurdeux_or with (A := B) (B := C) (C := B) (D := A);
[ intros H10; try clear orthogonal_pisurdeux_or
| intros H10; try clear orthogonal_pisurdeux_or
| auto
| auto
| auto with geo ].
cut (sin a 0); intros.
rewrite Rabs_right; auto with real.
apply triangle_rectangle_direct_sinus; auto.
replace (sin a) with (distance C B × / distance C A).
RReplace 0 (0 × / distance C A).
apply Rmult_ge_compat_r; auto with geo.
rewrite (triangle_rectangle_direct_sinus (A:=A) (B:=B) (C:=C) (a:=a)); intros;
auto with geo.
field.
auto with geo.
cut (- sin a 0); intros.
elim H6; clear H6; intros.
rewrite Rabs_left; auto with real.
apply triangle_rectangle_indirect_sinus; auto.
fourier.
rewrite Rabs_right; auto with real.
replace (sin a) with (- sin a).
apply triangle_rectangle_indirect_sinus; auto.
rewrite H6.
RReplace (sin a) (- - sin a).
rewrite H6; ring.
RReplace (sin a) (- - sin a).
rewrite H6; auto with real.
replace (- sin a) with (distance C B × / distance C A).
RReplace 0 (0 × / distance C A).
apply Rmult_ge_compat_r; auto.
rewrite (triangle_rectangle_indirect_sinus (A:=A) (B:=B) (C:=C) (a:=a));
intros; auto with geo.
field.
auto with geo.
Qed.

Lemma triangle_rectangle_direct_Sin :
A B C : PO,
A B
A C
B C
image_angle pisurdeux = cons_AV (vec B C) (vec B A) →
distance C B = distance C A × Sin (cons_AV (vec A B) (vec A C)).
intros.
mes (cons_AV (vec A B) (vec A C)).
rewrite <- H3.
rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=C) (x:=x)); auto.
apply triangle_rectangle_direct_sinus; auto.
Qed.

Lemma triangle_rectangle_indirect_Sin :
A B C : PO,
A B
A C
B C
image_angle (- pisurdeux) = cons_AV (vec B C) (vec B A) →
distance C B = distance C A × - Sin (cons_AV (vec A B) (vec A C)).
intros.
mes (cons_AV (vec A B) (vec A C)).
rewrite <- H3.
rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=C) (x:=x)); auto.
apply triangle_rectangle_indirect_sinus; auto.
Qed.

Lemma triangle_rectangle_absolu_Sin :
A B C : PO,
A B
A C
B C
orthogonal (vec B A) (vec B C) →
distance C B = distance C A × Rabs (Sin (cons_AV (vec A B) (vec A C))).
intros.
mes (cons_AV (vec A B) (vec A C)).
rewrite <- H3.
rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=C) (x:=x)); auto.
apply triangle_rectangle_absolu_sinus; auto.
Qed.

Lemma projete_negatif_cos :
(A B C H : PO) (a k : R),
A B
A C
H = projete_orthogonal A B C
vec A H = mult_PP k (vec A B) →
k < 0 → image_angle a = cons_AV (vec A B) (vec A C) → cos a < 0.
intros.
cut (scalaire (vec A B) (vec A C) < 0); intros.
replace (cos a) with
(/ distance A B × / distance A C × scalaire (vec A B) (vec A C)).
RReplace 0 (/ distance A B × / distance A C × 0).
apply Rmult_lt_compat_l; auto with real.
apply Rmult_lt_0_compat; auto with real.
apply Rinv_0_lt_compat; auto with real.
cut (distance A B 0); intros; auto with geo.
elim H7; auto with real; intros.
absurd (distance A B = 0); auto with geo.
apply Rinv_0_lt_compat; auto with real.
cut (distance A C 0); intros; auto with geo.
elim H7; auto with real; intros.
absurd (distance A C = 0); auto with geo.
rewrite (produit_scalaire_cosinus (A:=A) (B:=B) (C:=C) (a:=a)); auto.
field; split; auto with geo.
elim def_projete_orthogonal2 with (A := A) (B := B) (C := C) (H := H);
[ intros; auto | auto | auto ].
rewrite (scalaire_avec_projete (A:=A) (B:=B) (C:=C) (H:=H)); auto with geo.
rewrite H3.
RReplace (scalaire (vec A B) (mult_PP k (vec A B)))
(- (- k × scalaire (vec A B) (vec A B))).
apply Ropp_lt_gt_0_contravar; auto with real.
apply Rmult_gt_0_compat; auto with real.
cut (scalaire (vec A B) (vec A B) 0); intros; auto with geo.
elim H8; auto with real; intros.
absurd (scalaire (vec A B) (vec A B) = 0); auto with geo.
Simplscal.
Qed.

Lemma projete_absolu_cos :
(A B C H : PO) (a : R),
A B
A C
H = projete_orthogonal A B C
image_angle a = cons_AV (vec A B) (vec A C) →
distance A H = distance A C × Rabs (cos a).
intros.
elim def_projete_orthogonal2 with (A := A) (B := B) (C := C) (H := H);
[ intros; auto | auto | auto ].
halignes H4 ipattern:k.
cut (orthogonal (vec H A) (vec H C)); intros; auto with geo.
elim Rtotal_order with (r1 := k) (r2 := 0);
[ intros H8; try clear total_order
| intros H8; elim H8;
[ intros H9; try clear H8 | intros H9; try clear H8; try exact H9 ] ].
replace (Rabs (cos a)) with (Rabs (cos (a + pi))).
apply triangle_rectangle_absolu_cos; auto.
apply distinct_produit_vecteur with (3 := H6); auto with real.
rewrite H6; auto.
rewrite angle_produit_negatif_l; auto.
rewrite add_mes_compatible; rewrite <- H3; auto.
RReplace (a + pi) (pi + a).
elim pi_plus_x with (x := a);
[ intros H9 H10; try clear pi_plus_x; rewrite H9 ].
rewrite Rabs_Ropp; auto.
cut (A = H); intros.
rewrite <- H8 in H5; auto.
elim droit_direct_ou_indirect with (A := A) (B := B) (C := C);
[ intros H10; try clear droit_direct_ou_indirect
| intros H10; try clear droit_direct_ou_indirect; try exact H10
| auto
| auto
| auto ].
replace (cos a) with (cos pisurdeux).
rewrite cos_pisurdeux; rewrite Rabs_R0; ring_simplify.
rewrite <- H8; auto with geo.
apply cos_deux_mes.
rewrite H10; auto.
replace (cos a) with (cos (- pisurdeux)).
rewrite cos_paire; rewrite cos_pisurdeux; rewrite Rabs_R0; ring_simplify.
rewrite <- H8; auto with geo.
apply cos_deux_mes.
rewrite H10; auto.
apply produit_zero_conf with (1 := H6); auto.
apply triangle_rectangle_absolu_cos; auto.
apply distinct_produit_vecteur with (3 := H6); auto with real.
rewrite H6; auto.
rewrite angle_produit_positif_l; auto.
replace (vec H A) with (mult_PP (- k) (vec A B)).
Simplortho.
VReplace (vec H A) (mult_PP (-1) (vec A H)).
rewrite H6; Ringvec.
Qed.

Lemma projete_absolu_sin :
(A B C H : PO) (a : R),
triangle A B C
H = projete_orthogonal A B C
image_angle a = cons_AV (vec A B) (vec A C) →
distance C H = distance C A × Rabs (sin a).
intros.
deroule_triangle A B C.
elim def_projete_orthogonal2 with (A := A) (B := B) (C := C) (H := H);
[ intros; auto | auto | auto ].
halignes H7 ipattern:k.
cut (orthogonal (vec H A) (vec H C)); intros; auto with geo.
elim Rtotal_order with (r1 := k) (r2 := 0);
[ intros H11; try clear total_order
| intros H11; elim H11;
[ intros H12; try clear H11 total_order
| intros H12; try clear H11 total_order; try exact H12 ] ].
replace (Rabs (sin a)) with (Rabs (sin (a + pi))).
apply triangle_rectangle_absolu_sinus; auto.
apply distinct_produit_vecteur with (3 := H9); auto with real.
red in |- *; intros; apply H3.
rewrite <- H12; auto with geo.
rewrite H9.
rewrite angle_produit_negatif_l; auto.
rewrite add_mes_compatible; rewrite <- H2; auto.
RReplace (a + pi) (pi + a).
elim pi_plus_x with (x := a);
[ intros H12 H13; try clear pi_plus_x; rewrite H13 ].
rewrite Rabs_Ropp; auto.
cut (A = H); intros.
rewrite <- H13 in H8; auto.
elim droit_direct_ou_indirect with (A := A) (B := B) (C := C);
[ intros H14; try clear droit_direct_ou_indirect
| intros H14; try clear droit_direct_ou_indirect; try exact H14
| auto
| auto
| auto ].
replace (sin a) with (sin pisurdeux).
rewrite sin_pisurdeux; rewrite Rabs_R1; ring_simplify.
rewrite <- H13; auto.
apply sin_deux_mes.
rewrite H14; auto.
replace (sin a) with (sin (- pisurdeux)).
rewrite sin_impaire; rewrite sin_pisurdeux.
rewrite Rabs_Ropp; rewrite Rabs_R1; ring_simplify.
rewrite <- H13; auto.
apply sin_deux_mes.
rewrite H14; auto.
apply produit_zero_conf with (1 := H9); auto.
apply triangle_rectangle_absolu_sinus; auto.
apply distinct_produit_vecteur with (3 := H9); auto with real.
red in |- *; intros; apply H3.
rewrite <- H13; auto with geo.
rewrite H9; auto.
rewrite angle_produit_positif_l; auto.
replace (vec H A) with (mult_PP (- k) (vec A B)).
Simplortho.
VReplace (vec H A) (mult_PP (-1) (vec A H)).
rewrite H9; Ringvec.
Qed.

Lemma projete_absolu_Sin :
A B C H : PO,
triangle A B C
H = projete_orthogonal A B C
distance C H = distance C A × Rabs (Sin (cons_AV (vec A B) (vec A C))).
intros.
deroule_triangle A B C.
mes (cons_AV (vec A B) (vec A C)).
rewrite <- H6.
rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=C) (x:=x)); auto.
apply projete_absolu_sin with B; auto.
Qed.

Lemma projete_absolu_Cos :
A B C H : PO,
A B
A C
H = projete_orthogonal A B C
distance A H = distance A C × Rabs (Cos (cons_AV (vec A B) (vec A C))).
intros.
mes (cons_AV (vec A B) (vec A C)).
rewrite <- H3.
rewrite <- (egalite_cos_Cos (A:=A) (B:=B) (C:=C) (x:=x)); auto.
apply projete_absolu_cos with B; auto.
Qed.

Theorem Al_Kashi_Cos :
A B C : PO,
A B
A C
Rsqr (distance B C) =
Rsqr (distance A B) + Rsqr (distance A C) +
- (2 × (distance A B × (distance A C × Cos (cons_AV (vec A B) (vec A C))))).
unfold Rsqr in |- *; intros.
repeat rewrite <- carre_scalaire_distance.
rewrite (difference_Pythagore A B C).
rewrite (produit_scalaire_Cosinus (A:=A) (B:=B) (C:=C)); auto.
ring.
Qed.

Theorem Al_Kashi :
(A B C : PO) (a : R),
A B
A C
image_angle a = cons_AV (vec A B) (vec A C) →
Rsqr (distance B C) =
Rsqr (distance A B) + Rsqr (distance A C) +
- (2 × (distance A B × (distance A C × cos a))).
unfold Rsqr in |- *; intros.
repeat rewrite <- carre_scalaire_distance.
rewrite (difference_Pythagore A B C).
rewrite (produit_scalaire_cosinus (A:=A) (B:=B) (C:=C) (a:=a)); auto.
ring.
Qed.

Lemma triangles_isometriques :
(A B C : PO) (x y : R),
A B :>PO
A C :>PO
B C :>PO
distance = distance A B
distance = distance A C
cons_AV (vec A B) (vec A C) = cons_AV (vec ) (vec ) :>AV
image_angle x = cons_AV (vec B C) (vec B A) :>AV
image_angle = cons_AV (vec ) (vec ) :>AV
image_angle y = cons_AV (vec C A) (vec C B) :>AV
image_angle = cons_AV (vec ) (vec ) :>AV
distance = distance B C cos x = cos cos y = cos .
intros.
mesure A B A C.
cut ( ); intros.
elim H10; intros H22 H23; try clear H10.
cut (distance = distance B C); intros.
cut ( ).
intros H21.
cut (2 0).
intros H24.
split; [ try assumption | idtac ].
split; [ try assumption | idtac ].
cut
(Rsqr (distance C A) =
Rsqr (distance B C) + Rsqr (distance B A) +
- (2 × (distance B C × (distance B A × cos x))));
intros.
cut
(Rsqr (distance ) =
Rsqr (distance ) + Rsqr (distance ) +
- (2 × (distance × (distance × cos ))));
intros.
cut
(2 × (distance B C × distance B A) × cos x =
2 × (distance × distance ) × cos );
intros.
apply
resolution2
with
(x := 2 × (distance B C × distance B A))
(y := 2 × (distance × distance )); auto with geo real.
rewrite (distance_sym ); rewrite H10; rewrite H2;
rewrite (distance_sym B A); ring.
replace (2 × (distance × distance ) × cos ) with
(Rsqr (distance ) + Rsqr (distance ) + - Rsqr (distance )).
replace (2 × (distance B C × distance B A) × cos x) with
(Rsqr (distance B C) + Rsqr (distance B A) + - Rsqr (distance C A)).
rewrite (distance_sym ); rewrite (distance_sym ); rewrite H10;
rewrite H2; rewrite H3; rewrite (distance_sym B A);
rewrite (distance_sym C A); ring.
rewrite H11; ring.
rewrite H12; ring.
apply Al_Kashi; auto.
apply Al_Kashi; auto.
cut
(Rsqr (distance A B) =
Rsqr (distance C A) + Rsqr (distance C B) +
- (2 × (distance C A × (distance C B × cos y))));
intros.
cut
(Rsqr (distance ) =
Rsqr (distance ) + Rsqr (distance ) +
- (2 × (distance × (distance × cos ))));
intros.
cut
(2 × (distance C A × distance C B) × cos y =
2 × (distance × distance ) × cos );
intros.
apply
resolution2
with
(x := 2 × (distance C A × distance C B))
(y := 2 × (distance × distance )); auto with geo real.
rewrite (distance_sym ); rewrite H3; rewrite (distance_sym );
rewrite H10; rewrite (distance_sym C B); rewrite (distance_sym C A);
ring.
replace (2 × (distance C A × distance C B) × cos y) with
(Rsqr (distance C A) + Rsqr (distance C B) + - Rsqr (distance A B)).
replace (2 × (distance × distance ) × cos ) with
(Rsqr (distance ) + Rsqr (distance ) + - Rsqr (distance )).
rewrite (distance_sym ); rewrite (distance_sym ); rewrite H10;
rewrite H2; rewrite H3; rewrite (distance_sym C B);
rewrite (distance_sym C A); ring.
rewrite H12; ring.
rewrite H11; ring.
apply Al_Kashi; auto.
apply Al_Kashi; auto.
discrR.
apply dist_non_nulle; rewrite H10; auto with geo.
apply distance_carre; auto.
mesure A B A C.
rewrite (Al_Kashi (A:=) (B:=) (C:=) (a:=x0)); auto.
rewrite (Al_Kashi (A:=A) (B:=B) (C:=C) (a:=x0)); auto.
rewrite H2; rewrite H3; ring.
rewrite H9; rewrite H4; auto.
split; [ idtac | try assumption ].
apply dist_non_nulle; rewrite H2; auto with geo.
apply dist_non_nulle; rewrite H3; auto with geo.
Qed.

Axiom
angles_egaux_triangle :
(A B C : PO) (x y : R),
A B :>PO
A C :>PO
B C :>PO
cons_AV (vec A B) (vec A C) = cons_AV (vec ) (vec ) :>AV
image_angle x = cons_AV (vec B C) (vec B A) :>AV
image_angle = cons_AV (vec ) (vec ) :>AV
image_angle y = cons_AV (vec C A) (vec C B) :>AV
image_angle = cons_AV (vec ) (vec ) :>AV
cos x = cos
cos y = cos
cons_AV (vec B C) (vec B A) = cons_AV (vec ) (vec ) :>AV
cons_AV (vec C A) (vec C B) = cons_AV (vec ) (vec ) :>AV.

Lemma cas_egalite_triangle :
A B C : PO,
A B :>PO
A C :>PO
B C :>PO
distance = distance A B
distance = distance A C
cons_AV (vec A B) (vec A C) = cons_AV (vec ) (vec ) :>AV
distance = distance B C
cons_AV (vec B C) (vec B A) = cons_AV (vec ) (vec ) :>AV
cons_AV (vec C A) (vec C B) = cons_AV (vec ) (vec ) :>AV.
intros.
cut ( ); intros.
elim H5; intros H6 H7; try clear H5; try exact H7.
mesure A B A C.
cut (distance = distance B C).
intros H20.
cut ( ).
intros H21.
mesure B C B A.
mesure .
mesure C A C B.
mesure .
rewrite H11; rewrite H10; rewrite H9; rewrite H8.
elim
triangles_isometriques
with
(A := A)
(B := B)
(C := C)
( := )
( := )
( := )
(x := x0)
( := x1)
(y := x2)
( := x3);
[ intros; try exact H0
| auto
| auto
| auto
| auto
| auto
| auto
| auto
| auto
| auto
| auto ].
split; [ try assumption | idtac ].
elim H13; intros H14 H15; try clear H13; try exact H15.
apply angles_egaux_triangle with (9 := H14) (10 := H15); auto.
apply dist_non_nulle; rewrite H20; auto with geo.
cut (Rsqr (distance ) = Rsqr (distance B C)); intros.
apply resolution; auto with geo real.
rewrite (Al_Kashi (A:=) (B:=) (C:=) (a:=x)); auto.
rewrite (Al_Kashi (A:=A) (B:=B) (C:=C) (a:=x)); auto.
rewrite H2; rewrite H3; ring.
rewrite H5; rewrite H4; auto.
split; [ idtac | try assumption ].
apply dist_non_nulle; rewrite H2; auto with geo.
apply dist_non_nulle; rewrite H3; auto with geo.
Qed.

Lemma triangles_isometriques_indirects :
(A B C : PO) (x y : R),
A B :>PO
A C :>PO
B C :>PO
distance = distance A B
distance = distance A C
cons_AV (vec A B) (vec A C) = cons_AV (vec ) (vec ) :>AV
image_angle x = cons_AV (vec B C) (vec B A) :>AV
image_angle = cons_AV (vec ) (vec ) :>AV
image_angle y = cons_AV (vec C A) (vec C B) :>AV
image_angle = cons_AV (vec ) (vec ) :>AV
distance = distance B C cos x = cos cos y = cos .
intros.
mesure A B A C.
cut ( ); intros.
elim H10; intros H22 H23; try clear H10.
cut (distance = distance B C); intros.
cut ( ).
intros H21.
cut (2 0).
intros H24.
split; [ try assumption | idtac ].
split; [ try assumption | idtac ].
cut
(Rsqr (distance C A) =
Rsqr (distance B C) + Rsqr (distance B A) +
- (2 × (distance B C × (distance B A × cos x))));
intros.
cut
(Rsqr (distance ) =
Rsqr (distance ) + Rsqr (distance ) +
- (2 × (distance × (distance × cos ))));
intros.
cut
(2 × (distance B C × distance B A) × cos x =
2 × (distance × distance ) × cos );
intros.
apply
resolution2
with
(x := 2 × (distance B C × distance B A))
(y := 2 × (distance × distance )); auto with geo real.
rewrite (distance_sym ); rewrite H10; rewrite H2;
rewrite (distance_sym B A); ring.
replace (2 × (distance × distance ) × cos ) with
(Rsqr (distance ) + Rsqr (distance ) + - Rsqr (distance )).
replace (2 × (distance B C × distance B A) × cos x) with
(Rsqr (distance B C) + Rsqr (distance B A) + - Rsqr (distance C A)).
rewrite (distance_sym ); rewrite (distance_sym ); rewrite H10;
rewrite H2; rewrite H3; rewrite (distance_sym B A);
rewrite (distance_sym C A); ring.
rewrite H11; ring.
rewrite H12; ring.
apply Al_Kashi; auto.
apply Al_Kashi; auto.
cut
(Rsqr (distance A B) =
Rsqr (distance C A) + Rsqr (distance C B) +
- (2 × (distance C A × (distance C B × cos y))));
intros.
cut
(Rsqr (distance ) =
Rsqr (distance ) + Rsqr (distance ) +
- (2 × (distance × (distance × cos ))));
intros.
cut
(2 × (distance C A × distance C B) × cos y =
2 × (distance × distance ) × cos );
intros.
apply
resolution2
with
(x := 2 × (distance C A × distance C B))
(y := 2 × (distance × distance )); auto with geo real.
rewrite (distance_sym ); rewrite H3; rewrite (distance_sym );
rewrite H10; rewrite (distance_sym C B); rewrite (distance_sym C A);
ring.
replace (2 × (distance C A × distance C B) × cos y) with
(Rsqr (distance C A) + Rsqr (distance C B) + - Rsqr (distance A B)).
replace (2 × (distance × distance ) × cos ) with
(Rsqr (distance ) + Rsqr (distance ) + - Rsqr (distance )).
rewrite (distance_sym ); rewrite (distance_sym ); rewrite H10;
rewrite H2; rewrite H3; rewrite (distance_sym C B);
rewrite (distance_sym C A); ring.
rewrite H12; ring.
rewrite H11; ring.
apply Al_Kashi; auto.
apply Al_Kashi; auto.
discrR.
apply dist_non_nulle; rewrite H10; auto with geo.
apply distance_carre.
mesure A B A C.
rewrite (Al_Kashi (A:=A) (B:=B) (C:=C) (a:=x1)); auto.
rewrite (Al_Kashi (A:=) (B:=) (C:=) (a:=- x1)); auto.
rewrite H2; rewrite H3; rewrite cos_paire; ring.
apply (mes_oppx (A:=) (B:=) (C:=) (D:=) (x:=x1)); auto.
rewrite H10; rewrite H4; auto.
split; [ idtac | try assumption ].
apply dist_non_nulle; rewrite H2; auto with geo.
apply dist_non_nulle; rewrite H3; auto with geo.
Qed.

Axiom
angles_egaux_triangle_indirect :
(A B C : PO) (x y : R),
A B :>PO
A C :>PO
B C :>PO
cons_AV (vec A B) (vec A C) = cons_AV (vec ) (vec ) :>AV
image_angle x = cons_AV (vec B C) (vec B A) :>AV
image_angle = cons_AV (vec ) (vec ) :>AV
image_angle y = cons_AV (vec C A) (vec C B) :>AV
image_angle = cons_AV (vec ) (vec ) :>AV
cos x = cos :>R
cos y = cos :>R
cons_AV (vec B C) (vec B A) = cons_AV (vec ) (vec ) :>AV
cons_AV (vec C A) (vec C B) = cons_AV (vec ) (vec ) :>AV.

Lemma cas_egalite_triangle_indirect :
A B C : PO,
A B :>PO
A C :>PO
B C :>PO
distance = distance A B :>R
distance = distance A C :>R
cons_AV (vec A B) (vec A C) = cons_AV (vec ) (vec ) :>AV
distance = distance B C :>R
cons_AV (vec B C) (vec B A) = cons_AV (vec ) (vec ) :>AV
cons_AV (vec C A) (vec C B) = cons_AV (vec ) (vec ) :>AV.
intros.
cut ( ); intros.
elim H5; intros H6 H7; try clear H5; try exact H7.
mesure A B A C.
cut (distance = distance B C).
intros H20.
cut ( ).
intros H21.
mesure B C B A.
mesure .
mesure C A C B.
mesure .
rewrite H8; rewrite H10; rewrite H11.
elim
triangles_isometriques_indirects
with
(A := A)
(B := B)
(C := C)
( := )
( := )
( := )
(x := x0)
( := x1)
(y := x2)
( := x3);
[ intros; try exact H0
| auto
| auto
| auto
| auto
| auto
| auto
| auto
| auto
| auto
| auto ].
split; [ try assumption | idtac ].
elim H13; intros H14 H15; try clear H13; try exact H15.
apply
angles_egaux_triangle_indirect
with (x := x0) ( := x1) (y := x2) ( := x3); auto.
apply dist_non_nulle; rewrite H20; auto with geo.
apply distance_carre.
rewrite (Al_Kashi (A:=A) (B:=B) (C:=C) (a:=x)); auto.
rewrite (Al_Kashi (A:=) (B:=) (C:=) (a:=- x)); auto.
rewrite H2; rewrite H3; rewrite cos_paire; ring.
apply (mes_oppx (A:=) (B:=) (C:=) (D:=) (x:=x)); auto.
rewrite H5; rewrite H4; auto.
split; [ idtac | try assumption ].
apply dist_non_nulle; rewrite H2; auto with geo.
apply dist_non_nulle; rewrite H3; auto with geo.
Qed.