proposition: Lemma rotation_IAB : forall (I A B A' B' : PO) (a : R), I <> A -> I <> B -> A' = rotation I a A -> B' = rotation I a B -> cons_AV (vec I A) (vec I B) = cons_AV (vec I A') (vec I B') :>AV.
proof: Proof. intros. generalize (isometrie_distinct (A:=I) (B:=B) (A':=I) (B':=B')); intros. generalize (isometrie_distinct (A:=I) (B:=A) (A':=I) (B':=A')); intros. elim rotation_def with (I := I) (A := B) (B := B') (a := a); [ try clear rotation_def; intros | auto | auto ]. elim rotation_def with (I := I) (A := A) (B := A') (a := a); [ try clear rotation_def; intros | auto | auto ]. replace (cons_AV (vec I A') (vec I B')) with (plus (cons_AV (vec I A') (vec I A)) (plus (cons_AV (vec I A) (vec I B)) (cons_AV (vec I B) (vec I B')))). rewrite <- H6. rewrite <- (mes_oppx (A:=I) (B:=A) (C:=I) (D:=A') (x:=a)); auto. mesure I A I B. replace (- a + (x + a)) with x; try ring; auto. rewrite Chasles; auto. rewrite Chasles; auto. Qed.