proposition: Lemma half_nneg : forall q, 0 <= q -> 0 <= q / 2%nat.
proof: Proof. intros q H. apply Qcmult_lt_0_le_reg_r with 2%nat. now compute. rewrite Qcmult_0_l. unfold Qcdiv. rewrite <- Qcmult_assoc. rewrite Qcmult_inv_l. now rewrite Qcmult_1_r. now compute. Qed.
imports: Qfield Qreduction Qcanon