proposition: Lemma homothetie_conserve_angle : forall (I A B C A' B' C' : PO) (k : R), k <> 0 -> A <> B -> A <> C -> A' = homothetie k I A -> B' = homothetie k I B -> C' = homothetie k I C -> cons_AV (vec A B) (vec A C) = cons_AV (vec A' B') (vec A' C').
proof: Proof. intros. cut (vec A' B' = mult_PP k (vec A B)); intros. cut (vec A' C' = mult_PP k (vec A C)); intros. cut (A' <> B'); intros. cut (A' <> C'); intros. rewrite H5. elim Rtotal_order with (r1 := k) (r2 := 0); intros. rewrite angle_produit_negatif_l; auto. rewrite H6. rewrite angle_produit_negatif_r2; auto. rewrite <- plus_associative. rewrite <- add_mes_compatible. replace (pi + pi) with deuxpi; auto. rewrite pi_plus_pi. rewrite plus_angle_zero; auto. elim H9; [ intros H10; try clear H9 | intros H10; try clear H9; try exact H10 ]. absurd (k = 0); auto with real. rewrite angle_produit_positif_l; auto. rewrite H6. rewrite angle_produit_positif_r2; auto. apply image_homothetie_distincts with (3 := H2) (4 := H4); auto. apply image_homothetie_distincts with (3 := H2) (4 := H3); auto. apply homothetie_bipoint with I; auto. apply homothetie_bipoint with I; auto. Qed.