proposition: Lemma paralleles_dilatations : forall A A' B B' : PO, A <> B -> A' <> B' -> paralleles (droite A' B') (droite A B) -> (exists I : PO, (exists J : PO, A' = translation I J A /\ B' = translation I J B)) \/ (exists k : R, (exists I : PO, A' = homothetie k I A /\ B' = homothetie k I B)).
proof: Proof. intros. elim paralleles_vecteur with (A := A') (B := B') (C := A) (D := B); [ intros k H2; try clear paralleles_vecteur; try exact H2 | trivial | trivial | trivial ]. elim (classic (k = 0)); intros; auto. absurd (A' = B'); intros; auto. apply vecteur_nul_conf; auto. rewrite H2; rewrite H3; Ringvec. elim (classic (k = 1)); intros; auto. rewrite H4 in H2. left; try assumption. exists A; exists A'. split; apply rec_translation_vecteur; auto. apply egalite_vecteur; rewrite H2; Ringvec. right; try assumption. exists k; exists (barycentre (cons (- k) A) (cons 1 A')). cut (A' = homothetie k (barycentre (cons (- k) A) (cons 1 A')) A). intros H20. split; [ try assumption | idtac ]. apply vecteur_homothetie. replace (vec (barycentre (cons (- k) A) (cons 1 A')) B') with (add_PP (vec (barycentre (cons (- k) A) (cons 1 A')) A') (vec A' B')). cut (vec (barycentre (cons (- k) A) (cons 1 A')) A' = mult_PP k (vec (barycentre (cons (- k) A) (cons 1 A')) A)); intros. rewrite H5; rewrite H2; Ringvec. apply homothetie_vecteur; auto. Ringvec. unfold homothetie in |- *. replace (1 + - k) with (- k + 1); try ring; auto. apply conversion_PP with (a := 1) (b := 1); auto with real. pattern 1 at 2 in |- *. replace 1 with (k + (- k + 1)); try ring; auto. rewrite <- add_PP_barycentre; auto. rewrite <- add_PP_barycentre; auto. RingPP. red in |- *; intros; apply H4. replace 1 with (k + (- k + 1)). rewrite H5; try ring. ring. replace (k + (- k + 1)) with 1; try ring; auto with real. Qed.