proposition: Lemma euclid_lemma p t : (p + t = size (r 0))%N -> let stop := stop t (r 0) (r 1) in size (v stop) <= p /\ size (r stop) <= t.
proof: Proof. move=> H. case/boolP : (0 < size r0) => [Hr0|]; last first. rewrite -leqNgt leqn0 size_poly_eq0 => /eqP ?; subst r0. suff : p = O /\ t = O. case=> -> -> /=. rewrite /stop. case: Bool.bool_dec => [H1|_]. exfalso. by rewrite size_poly0 ltnn in H1. by rewrite /= /Euclid.v0 size_poly0. move: H; rewrite size_poly0. by case: p. move=> j. case/boolP : (t < size r0) => Hnu; last first. have {Hnu} ?: p = O. move: Hnu. rewrite -H -leqNgt. by rewrite -{2}(add0n t) leq_add2r leqn0 => /eqP. subst p. rewrite {}/j. rewrite /stop. case: Bool.bool_dec => H1. exfalso. move: H1. by rewrite -H add0n ltnn. by rewrite /= /Euclid.v0 size_poly0 leqnn -H add0n. split; last by apply: stop_is_after. rewrite -(leq_add2r t) H. move: (@relationF _ _ _ _ (stop' Hnu r1_leq_r0) Hnu r1_leq_r0). rewrite /stop. case: Bool.bool_dec => H1; last by rewrite Hnu in H1. case: Bool.bool_dec => H2; last by rewrite r1_leq_r0 in H2. rewrite (_ : H1 = Hnu); last by apply eq_irrelevance. rewrite (_ : H2 = r1_leq_r0); last by apply eq_irrelevance. rewrite ltnSn => /(_ isT). rewrite -/(stop _ _) => /(congr1 (fun x => x.+1)). rewrite prednK ?lt0n ?size_poly_eq0 //; last by rewrite -size_poly_eq0 -lt0n. move => <-. rewrite -ltnS. move: (stop'_is_before Hnu r1_leq_r0) => Hsave; move: (Hsave). rewrite -(ltn_add2l (size (v j))). move/leq_trans; apply. rewrite -addSn. case/boolP : (size (v j) == O) => vs0. rewrite (eqP vs0) add0n. rewrite addSn addnC -2!addSn (leq_trans _ (leq_addr _ _)) // prednK //. by rewrite (leq_trans _ Hsave). rewrite /j /stop. case: Bool.bool_dec => H1'; last by rewrite Hnu in H1. case: Bool.bool_dec => H2'; last by rewrite r1_leq_r0 in H2. rewrite -(_ : Hnu = H1'); last by apply eq_irrelevance. rewrite -(_ : r1_leq_r0 = H2'); last by apply eq_irrelevance. rewrite -addnS leq_add // prednK // ?(leq_trans _ Hsave) // ?lt0n. apply: contra vs0. rewrite /j /stop. case: Bool.bool_dec => H1''; last by rewrite Hnu in H1. case: Bool.bool_dec => H2''; last by rewrite r1_leq_r0 in H2. rewrite -(_ : Hnu = H1''); last by apply eq_irrelevance. rewrite -(_ : r1_leq_r0 = H2'') //; by apply eq_irrelevance. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv matrix)