proposition: Lemma Qmult_mult_Qle_Qone_Qopp_Qone: forall q, -Qone<=q -> q<= Qone -> q*q <= Qone.
proof: Proof. intros q H1 H2. destruct (Q_le_lt_dec Zero q). stepr (Qone*Qone); trivial; apply Qmult_Qle_compat; assumption. stepl ((-q)*(-q)); [|ring]; stepr (Qone*Qone); trivial; apply Qmult_Qle_compat; auto; apply Qle_opp; stepr q; auto; ring. Qed.