proposition: Lemma sub_sternD a b c d n: c <= a -> d <= b -> sternD (a - c) (b - d) n = sub_seq (sternD a b n) (sternD c d n).
proof: Proof. set x := (sternD (a - c) (b - d) n). move => ha hb;rewrite - (subnKC ha) - (subnKC hb) add_sternD -/x. have: size x == size (sternD c d n) by rewrite !size_sternD. move: x (sternD c d n); apply: seq2_ind => // e f s1 s2. by rewrite /sub_seq /= addKn => {1} ->. 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)