Library mathcomp_eulerian.qbin

From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GRing.Theory.
Local Open Scope ring_scope.


Fixpoint qbin (n k : nat) : {poly int} :=
  match n, k with
  | _, 0%N ⇒ 1
  | 0%N, _.+1 ⇒ 0
  | n'.+1, k'.+1 ⇒ qbin n' k' + 'X^(k'.+1) × qbin n' k'.+1
  end.

Lemma qbin_n0 n : qbin n 0 = 1.
Proof. by case: n. Qed.

Lemma qbin_0S k : qbin 0 k.+1 = 0.
Proof. by []. Qed.

Lemma qbinS n k :
  qbin n.+1 k.+1 = qbin n k + 'X^(k.+1) × qbin n k.+1.
Proof. by []. Qed.


Lemma qbin_small n k : (n < k)%N → qbin n k = 0.
Proof.
elim: n k ⇒ [|n IHn] [|k] // lt_nk.
by rewrite qbinS !IHn // ?mulr0 ?addr0 // ltnW.
Qed.

Lemma qbin_nn n : qbin n n = 1.
Proof.
elim: n ⇒ [|n IHn] //.
by rewrite qbinS IHn qbin_small // mulr0 addr0.
Qed.


Lemma qbin_horner1 n k : (qbin n k).[1] = ('C(n, k))%:R.
Proof.
elim: n k ⇒ [|n IHn] [|k]; rewrite ?qbin_n0 ?hornerC ?bin0 //.
rewrite qbinS hornerD hornerM hornerXn expr1n mul1r !IHn.
by rewrite binS natrD addrC.
Qed.