proposition: Lemma cnf_and_val_pb x: cnfp x -> cnf_and_val x (cnf_val x).
proof: Proof. move => h; hnf. move:(h) => [ha hb hc hd]. move: (OS_CNFb hb hd) => ot; split => //. move: (the_cnf_p0 ot) => [qa qb]; exact (cnf_val_inj qa h qb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)