proposition: Lemma Stern_consecutive_sym a b: Stern_consecutive a b -> Stern_consecutive b a.
proof: Proof. move => [n [i [pa pb pc]]]. have pe: 2 ^ n - i.+1 < 2 ^ n by rewrite - {2} (subnK pa) ltn_paddr. have pf:(2 ^ n - i.+1).+1 < (2 ^ n).+1 by rewrite ltnS. have pg:2 ^ n - i.+1 < (2 ^ n).+1 by apply: ltnW. exists n, (2^n - i.+1). rewrite pe - stern11_symmetric! nth_rev size_sternD // subSS subKn // pc. by rewrite - {1} (subnK pa) addnS - !addSn addKn pb. 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)