proposition: Lemma sternD_split2 u v n: sternD u v n = rcons (belast u (behead (sternD u v n))) v.
proof: Proof. by rewrite - {3} (last_sternD u v n) {1 3}(sternD_split1 u v n) - lastI. 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)