proposition: Lemma definition_inversion : forall (I A B : PO) (k : R), k <> 0 -> I <> A -> (B = inversion I k A <-> alignes I A B /\ scalaire (vec I A) (vec I B) = k).
proof: Proof. intros; red in |- *; try split; intros. apply inversion_def; auto. apply inversion_def2; tauto. Qed.