proposition: Lemma istep_algo n p : (size p <= 2 ^ n)%N -> istep n p = algo n p.
proof: Proof. move=> Hs. suff /(_ n 0%N): forall m1 n1 (p1 q1 : {poly R}), (size p1 <= 2 ^ (m1 + n1))%N -> (size q1 <= 2 ^ (m1 + n1))%N -> invariant_algo m1 n1 p1 q1 -> invariant_algo 0 (m1 + n1) p1 (istep_aux m1 n1 q1). rewrite addn0; apply => //; first by apply: size_bottom. by apply: invariant_algo_bottom. elim => [//| m1 IH] n1 p1 q1 Hs1 Hs2 H1. rewrite /istep_aux -/istep_aux addSnnS. apply: IH; first by rewrite addnS. rewrite addnS. by apply: leq_trans (size_step _ _ _) _. by apply: invariant_algo_step. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)