proposition: Lemma representant_unitaire_bis : forall A B : PO, A <> B :>PO -> representant_unitaire (representant_unitaire (vec A B)) = representant_unitaire (vec A B) :>PP.
proof: Proof. intros A B H; try assumption. elim existence_representant_unitaire with (A := A) (B := B); [ intros B' H3; try clear existence_representant_unitaire; rewrite <- H3 | auto ]. elim def_representant_unitaire2 with (A := A) (B := B) (C := B'); [ intros | auto | auto ]. elim H1; intros H2 H4; try clear H1; try exact H4. cut (A <> B'); intros; auto with geo. elim existence_representant_unitaire with (A := A) (B := B'); [ intros C' H5; rewrite <- H5; intros | auto ]. elim def_representant_unitaire2 with (A := A) (B := B') (C := C'); [ intros | auto | auto ]. elim H7; intros H8 H9; try clear H7; try exact H9. cut (A <> C'); intros; auto with geo. halignes H6 k. elim Rtotal_order with (r1 := k) (r2 := 0); [ intros H13 | intros H13; (elim H13; [ intros H14; try clear H13 | intros H14; try clear H13; try exact H14 ]) ]. absurd (scalaire (vec A B') (vec A C') >= 0); auto. rewrite H10. replace (scalaire (vec A B') (mult_PP k (vec A B'))) with (k * scalaire (vec A B') (vec A B')); [ idtac | Simplscal ]. rewrite H2. replace (k * 1) with k; [ auto with real | ring ]. absurd (A = C'); auto with geo. apply vecteur_nul_conf. rewrite H10; rewrite H14; Ringvec. elim (classic (k = 1)); intros. rewrite H10; rewrite H11; Ringvec. absurd (scalaire (vec A C') (vec A C') = 1); auto. rewrite H10; Simplscal; rewrite H2. replace (k * k * 1) with (Rsqr k) by (unfold Rsqr; ring). red in |- *; intros; apply H11. apply Rsqr_inj; auto with real. rewrite H12; unfold Rsqr in |- *; ring. Qed.