proposition: Lemma BZ_induction_neg a (r:property): (r a) -> (forall n, n <=z a -> r n -> r (BZpred n)) -> (forall n, n <=z a -> r n).
proof: Proof. move => pb pc n h; move: (h) => [pa pd _]. move: (zle_opp h) => pe. rewrite - (BZopp_K pa); pose s n:= r (BZopp n); rewrite -/(s _). move: pb ; rewrite - (BZopp_K pd); rewrite -/(s _) => sa. apply: (BZ_induction_pos sa _ pe). move => m le1; move: (zle_opp le1); rewrite (BZopp_K pd) /s /BZsucc. rewrite (BZoppD (proj32 le1) ZS1); apply: pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)