proposition: Lemma sternD_col_progression n i : i <= 2^n -> nth 0 (stern11 n.+1) i = nth 0 (stern11 n) i + stern i.
proof: Proof. move => lin. have s1: size (stern01 n) = (2 ^n).+1 by rewrite size_sternD. have s2: size (stern11 n) = (2 ^n).+1 by rewrite size_sternD. have s3: size (sternD 0 1 n) = size (sternD 1 1 n) by rewrite s1 s2. have ib2 : i < size (zip (stern01 n) (stern11 n)). by rewrite size_zip s1 s2 minnn. transitivity (nth 0 (sternD 1 2 n) i). by rewrite - (split_sternD_left 1 1 n) nth_take. rewrite (add_sternD 0 1 1 1 n) /add_seq (nth_map (0, 0)) //. by rewrite nth_zip // addnC stern_prop. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)