proposition: Lemma diametre_rectangle : forall A B C C' : PO, A <> B -> C' = milieu A B -> distance C' C = distance C' A -> orthogonal (vec C A) (vec C B).
proof: Proof. intros. discrimine C A. apply ortho_sym. replace (vec A A) with zero. apply zero_ortho_tout. Ringvec. discrimine C B. replace (vec B B) with zero. apply zero_ortho_tout. Ringvec. cut (B <> C'); intros. cut (A <> C'); intros. cut (C <> C'); intros. apply angles_orthogonal; auto. cut (isocele C' C A); intros. cut (isocele C' B C); intros. generalize (isocele_angles_base (A:=C') (B:=C) (C:=A)); auto; intros. generalize (isocele_angles_base (A:=C') (B:=B) (C:=C)); auto; intros. generalize (somme_triangle (A:=C') (B:=C) (C:=A)); intros. generalize (somme_triangle (A:=C') (B:=B) (C:=C)); intros. replace (double_AV (cons_AV (vec C A) (vec C B))) with (plus (double_AV (cons_AV (vec C A) (vec C C'))) (double_AV (cons_AV (vec C C') (vec C B)))). replace (double_AV (cons_AV (vec C A) (vec C C'))) with (plus (cons_AV (vec C A) (vec C C')) (cons_AV (vec A C') (vec A C))). replace (double_AV (cons_AV (vec C C') (vec C B))) with (plus (cons_AV (vec B C) (vec B C')) (cons_AV (vec C C') (vec C B))). replace (plus (cons_AV (vec B C) (vec B C')) (cons_AV (vec C C') (vec C B))) with (plus (image_angle pi) (opp (cons_AV (vec C' B) (vec C' C)))). replace (plus (cons_AV (vec C A) (vec C C')) (cons_AV (vec A C') (vec A C))) with (plus (image_angle pi) (opp (cons_AV (vec C' C) (vec C' A)))). rewrite def_opp; auto. rewrite def_opp; auto. mesure C' A C' C. mesure C' C C' B. replace (pi + x + (pi + x0)) with (pi + pi + (x + x0)). replace (pi + pi) with deuxpi; auto. rewrite add_mes_compatible; rewrite pi_plus_pi; rewrite <- add_mes_compatible. replace (0 + (x + x0)) with (x + x0); auto. rewrite add_mes_compatible. rewrite H14; rewrite H13. replace (plus (cons_AV (vec C' A) (vec C' C)) (cons_AV (vec C' C) (vec C' B))) with (cons_AV (vec C' A) (vec C' B)). rewrite <- (milieu_vecteur (A:=A) (B:=B) (M:=C')); auto. rewrite <- angle_plat; auto. rewrite Chasles; auto. ring. ring. rewrite <- H11; auto. rewrite <- H9; auto. mesure C' C C' A. mesure C A C C'. replace (x + (x0 + x0) + - x) with (x0 + x0); auto. ring. rewrite <- H12; auto. rewrite <- H10; auto. mesure C' B C' C. mesure B C B C'. replace (x + (x0 + x0) + - x) with (x0 + x0); auto. ring. rewrite H10; auto. rewrite H9; auto. rewrite double_Chasles; auto. unfold isocele in |- *. rewrite H1. apply carre_scalaire_egalite_distance. rewrite <- (milieu_vecteur (A:=A) (B:=B) (M:=C')); auto. replace (vec A C') with (mult_PP (-1) (vec C' A)); auto. Simplscal. Ringvec. unfold isocele in |- *. rewrite H1; auto. apply isometrie_distinct with (1 := H5). rewrite distance_sym. rewrite <- H1; rewrite distance_sym; auto. rewrite H0. apply milieu_distinct; auto. rewrite H0. apply milieu_distinct2; auto. Qed.