proposition: Lemma inversion_involution : forall (I A B : PO) (k : R), k <> 0 -> I <> A -> B = inversion I k A -> A = inversion I k B.
proof: Proof. intros. deroule_inversion I A B k. apply inversion_def2; auto. auto with geo. rewrite <- H3; auto with geo. apply scalaire_sym. Qed.