proposition: Lemma inversion_droite_pole : forall (A A' M M' I : PO) (k : R), k <> 0 -> I <> A -> I <> M -> alignes I A M -> A' = inversion I k A -> M' = inversion I k M -> alignes I A A' /\ alignes I A' M'.
proof: Proof. intros. deroule_inversion I M M' k. deroule_inversion I A A' k. assert (A = inversion I k A'); auto with geo. deroule_inversion I A' A k. split; [ try assumption | idtac ]. halignes H12 a. halignes H5 b. halignes H2 c. apply colineaire_alignes with (a * (b * c)). rewrite H16; rewrite H17; rewrite H15. Ringvec. Qed.