proposition: Lemma OS_cnf_valp x: cnfp_nz x -> \0o <o (cnf_val x).
proof: Proof. move => ox. move: (cnf_size_nz ox) => [qa qb]. move:(proj44 (proj1 ox)); rewrite /cnf_val qb => ax1. exact: (CNFq_pg5 qa ax1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)