proposition: Lemma similitude_conserve_angle : forall (I A B C A' B' C' : PO) (k a : R), k > 0 -> A <> B -> A <> C -> A' = similitude I k a A -> B' = similitude I k a B -> C' = similitude I k a C -> cons_AV (vec A B) (vec A C) = cons_AV (vec A' B') (vec A' C').
proof: Proof. intros. elim similitude_decomposition with (I := I) (M := A) (M' := A') (k := k) (a := a); [ intros A1 H7; elim H7; intros H8 H9; try clear H7 | auto | auto ]. elim similitude_decomposition with (I := I) (M := B) (M' := B') (k := k) (a := a); [ intros B1 H7; elim H7; intros H10 H11; try clear H7; try exact H11 | auto | auto ]. elim similitude_decomposition with (I := I) (M := C) (M' := C') (k := k) (a := a); [ intros C1 H7; elim H7; intros H12 H13; try clear H7; try exact H13 | auto | auto ]. cut (A1 <> B1); intros. cut (A1 <> C1); intros. cut (cons_AV (vec A B) (vec A C) = cons_AV (vec A1 B1) (vec A1 C1)); intros. rewrite H7. apply (homothetie_conserve_angle (I:=I) (A:=A1) (B:=B1) (C:=C1) (A':=A') (B':=B') (C':=C') (k:=k)); auto with real. apply (rotation_conserve_angle (I:=I) (A:=A) (B:=B) (C:=C) (A':=A1) (B':=B1) (C':=C1) (a:=a)); auto. apply image_bipoint_distinct with (2 := H8) (3 := H12); auto. apply image_bipoint_distinct with (2 := H8) (3 := H10); auto. Qed.