proposition: Lemma induction_terms s a n: natp n -> induction_term s a (csucc n) = s n (induction_term s a n).
proof: Proof. move: (induction_defined_pr0 s a)=> [sf sjf w0 ws] nN. by rewrite /induction_term ws. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)