proposition: Lemma int_rect (P : int -> Type) : P 0 -> (forall n : nat, P n -> P (n.+1)%N) -> (forall n : nat, P (- (n%:Z)) -> P (- (n.+1%N%:Z))) -> forall n : int, P n.
proof: Proof. by move=> P0 hPp hPn []; elim=> [|n ihn]//; do ?[apply: hPn | apply: hPp]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)