proposition: Lemma pair_ind (P : nat -> Type) : P O -> P 1%nat -> (forall m, P m * P m.+1 -> P m.+2) -> forall m, P m.
proof: Proof. move=> P0 P1 H m. suff : (P m * P m.+1)%type by case. elim: m => // m [H1 H2]; split; by [assumption | apply H]. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)