len ((a,b) Subnomial ((n + 1) - 1)) = len (Newton_Coeff ((n + 1) - 1)) by DOMN;
hence len ((a,b) Subnomial ((n + 1) - 1)) = n + 1 ; :: thesis: verum