proposition: Lemma BZquo_val a b (q1:= ((BZ_val a) %/c (BZ_val b))) (q2 := BZ_of_nat q1): intp a -> intp b -> [/\ inc q1 Nat, inc q2 BZp & inc q2 BZ].
proof: Proof. move => az bz. move: (NS_quo (P b) (BZ_valN az)) => qb. by move: (BZ_of_natp_i qb) => pa; move: (BZp_sBZ pa) => pb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)