proposition: Lemma BZ_induction_pos a (r:property): (r a) -> (forall n, a <=z n -> r n -> r (BZsucc n)) -> (forall n, a <=z n -> r n).
proof: Proof. move => pb pc n h; move: (h) => [pa pd _]. move /(zle_diffP pa pd):h => dp. rewrite - (BZsum_diff pa pd) BZsumC - (BZp_hi_pr dp). move : (BZ_valN (BZp_sBZ dp)) => xn. pose s n := r ((BZ_of_nat n) +z a); rewrite -/(s _). apply: (Nat_induction _ _ xn); first by rewrite /s -/BZ_zero BZsum_0l. move => m mb; move:(BZ_of_natp_i mb) => aux1; move: (BZp_sBZ aux1) => aux. have : a <=z (BZ_of_nat m +z a). by apply/(zle_diffP pa (ZSs aux pa)); rewrite BZsumC (BZdiff_sum pa aux). rewrite /s - (BZsucc_N mb) (BZsucc_sum (BZ_of_nat_i mb) pa);apply:pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)