proposition: Lemma sternD_split1 u v n: sternD u v n = u :: behead (sternD u v n).
proof: Proof. rewrite -{2} (head_sternD u v n);move: (size_sternD u v n). by case:(sternD u v n). 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)