proposition: Lemma similitudes_meme_centre_commutent : forall (I M M1 M2 : PO) (k m a b : R), k > 0 -> m > 0 -> M1 = similitude I k a M -> M2 = similitude I m b M -> similitude I k a M2 = similitude I m b M1.
proof: Proof. intros I M M1 M2 k m a b H H0; try assumption. discrimine I M. repeat (rewrite <- similitude_def_centre; auto). intros H2 H3; try assumption. rewrite H2; rewrite H3. repeat (rewrite <- similitude_def_centre; auto). intros H2 H3; try assumption. elim existence_similitude_Ika with (I := I) (M := M1) (k := m) (a := b); [ intros N H4 | auto ]. elim existence_similitude_Ika with (I := I) (M := M2) (k := k) (a := a); [ intros M' H5 | auto ]. rewrite <- H5. cut (I <> M1); intros. 2: apply image_sim_distinct_centre with (3 := H2); auto. cut (I <> M2); intros. 2: apply image_sim_distinct_centre with (3 := H3); auto. cut (I <> M'); intros. 2: apply image_sim_distinct_centre with (3 := H5); auto. cut (I <> N); intros. 2: apply image_sim_distinct_centre with (3 := H4); auto. elim similitude_def with (I := I) (A := M2) (B := M') (k := k) (a := a); [ intros | auto | auto | auto ]. elim similitude_def with (I := I) (A := M1) (B := N) (k := m) (a := b); [ intros | auto | auto | auto ]. elim similitude_def with (I := I) (A := M) (B := M2) (k := m) (a := b); [ intros | auto | auto | auto ]. elim similitude_def with (I := I) (A := M) (B := M1) (k := k) (a := a); [ intros | auto | auto | auto ]. apply similitude_def2; auto. rewrite H16; rewrite H10; rewrite H14; ring. replace (cons_AV (vec I M1) (vec I M')) with (plus (plus (cons_AV (vec I M) (vec I M2)) (opp (cons_AV (vec I M) (vec I M1)))) (cons_AV (vec I M2) (vec I M'))). rewrite def_opp; auto. rewrite <- (mes_oppx (A:=I) (B:=M) (C:=I) (D:=M1) (x:=a)); auto. rewrite <- H15; rewrite <- H11. repeat rewrite <- add_mes_compatible. replace (b + - a + a) with b; auto. ring. rewrite Chasles_diff; auto. rewrite Chasles; auto. Qed.