proposition: Lemma alignes_diametre : forall A B A' : PO, alignes A A' B -> cercle_diametre A A' B -> B = A \/ B = A'.
proof: Proof. unfold cercle_diametre in |- *; intros. elim H0; [ intros O H1; elim H1; [ intros H2 H3; try clear H1 H0; try exact H3 ] ]. hcercle H2. discrimine A A'. assert (O = A). rewrite H3; rewrite <- H0; rewrite <- milieu_trivial; auto. rewrite <- H0. right; try assumption. rewrite <- H5. symmetry in |- *. assert (distance O B = 0); auto with geo. rewrite <- H4; rewrite <- H5; auto with geo. halignes H k. elim (classic (k = 0)); intros. left; symmetry in |- *. apply (produit_zero_conf H5); auto. discrimine O A. left; symmetry in |- *. assert (distance O B = 0); auto with geo. rewrite <- H4; rewrite <- H7; auto with geo. right; try assumption. assert (vec A B = mult_PP (2 * k) (vec A O)). rewrite H5. rewrite (milieu_vecteur_double H3); auto. Ringvec. assert (k = 1). assert (vec O B = mult_PP (1 + - (2 * k)) (vec O A)). VReplace (vec O B) (add_PP (vec A B) (vec O A)). rewrite H8; Ringvec. assert (Rsqr (1 + - (2 * k)) = 1). assert (Rsqr (distance O A) = Rsqr (1 + - (2 * k)) * Rsqr (distance O A)). pattern (distance O A) at 1 in |- *. rewrite H4. unfold Rsqr in |- *; repeat rewrite <- carre_scalaire_distance. rewrite H9. Simplscal. apply Rmult_eq_reg_l with (Rsqr (distance O A)). pattern (Rsqr (distance O A)) at 2 in |- *; rewrite H10 in |- *; ring. unfold Rsqr in |- *; apply Rmult_integral_contrapositive. split; auto with geo. assert (Rsqr (1 + - (2 * k)) + - Rsqr 1 = 0). rewrite H10; unfold Rsqr in |- *; ring. assert (2 * (1 + - k) * - (2 * k) = 0). RReplace (- (2 * k)) (1 + - (2 * k) + -1). RReplace (2 * (1 + - k)) (1 + - (2 * k) + 1). rewrite <- H11; unfold Rsqr in |- *; ring. assert (1 + - k = 0). apply Rmult_eq_reg_l with (- (2 * k)); auto with real. RReplace (- (2 * k) * 0) 0. apply Rmult_eq_reg_l with 2; auto with real. RReplace (2 * 0) 0. rewrite <- H12; ring. RReplace k (k + 0). rewrite <- H13; ring. apply egalite_vecteur_point with A. rewrite H5; rewrite H9; Ringvec. Qed.