proposition: Lemma Qinv_strext : forall (x y : Q) x_ y_, ~(Qinv_dep x x_==Qinv_dep y y_) -> ~(x==y).
proof: Proof. firstorder using Qinv_comp. Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q