proposition: Lemma ex4_length_prop1 x (n := ex4_last x): inc x ex4_F -> natp n /\ domain x = csucc n.
proof: Proof. move => / ex4_inF_hi [mz [ra _ _ _ _ _]]; exact:(cpred_pr ra mz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)