proposition: Lemma sternD_1n_disymmetric n q i j (S := sternD 1 n.+2 q) : i < j -> i + j = 2^q -> nth 0 S i < nth 0 S j.
proof: Proof. move => sa sb. have: i.*2 < 2^q by rewrite - sb - addnn ltn_add2l. rewrite /S; clear S; move: sa sb;case: q. rewrite expn0 ltnS (leq_double i 0) leqn0; move => sb sd sc; move: sd. rewrite (eqP sc) add0n => -> //. move => q sa sb; rewrite expn2S ltn_double => sc. have ->: j = 2 ^ q.+1 - i by rewrite - sb addKn. have h := ltnW sc. rewrite (sternD_1n_H1 _ h) (sternD_1n_H2' _ h). rewrite mulSn addnCA (mulSn n.+1) ltn_add2l ltn_add2l ltn_pmul2l //. rewrite (stern_prop h) (sternD_stern _ _ h) !mul1n. by rewrite ltn_paddl // stern_gt0 // subn_gt0. 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)