proposition: Lemma Qabs_Qminus_Zero_eq:forall q1 q2, Qabs (q1-q2) = Zero -> q1=q2.
proof: Proof. intros q1 q2 Hq; destruct (Q_zerop (q1-q2)) as [H|H]; auto; contradiction (Qlt_irreflexive Zero); stepr (Qabs (q1 - q2)); trivial; apply Qabs_nonzero_pos; trivial. Qed.