proposition: Lemma BQprod_Mltltge0 a b c d: inc a BQp -> inc c BQp -> a <q b -> c <q d -> (a *q c) <q (b *q d).
proof: Proof. move => pa pb pc pd. have H: (forall a b, inc a BQp -> a <q b -> inc b BQps). move => u v up uv; move: (uv) => [[uz vz _] _]. move/ (qlt_diffP uz vz): uv => pe; move: (QpsS_sum_r up pe). by rewrite BQsum_diff. move: (H _ _ pa pc) (H _ _ pb pd) => bp cp. case: (equal_or_not c \0q) => cnz. rewrite cnz BQprod_0r; [ by apply / qlt0xP; apply: QpsS_prod | BQo_tac ]. by apply: BQprod_Mltltgt0 => //; apply/ BQps_iP;split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)