proposition: Lemma zlt_P1 x y: inc x BZp -> inc y BZp -> (x <z y <-> (BZ_val x) <c (BZ_val y)).
proof: Proof. move => pa pb; split; move => [pc pd]; split. + by apply/(zle_P1 pa pb). + by dneg h; rewrite - (BZp_hi_pr pa) - (BZp_hi_pr pb) h. + by apply /(zle_P1 pa pb). + by dneg h; rewrite h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)