proposition: Lemma QpsS_fusc_quo n: natp n -> n <> \0c -> inc (fusc_quo n) BQps.
proof: Proof. move => nN nz. move:(NS_fusc nN)(NS_fusc (NS_succ nN))(fusc_nz nN nz)(fusc_nz' nN). by move => sa sb sc sd; apply:QpsS_div;apply:QpsS_of_nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)