proposition: Lemma mkseq_correct fv ft (mv mt : nat) : (forall k : nat, Rel (fv k) (ft k)) -> (forall k : nat, mv <= k < mt -> fv k = dv) -> (forall k : nat, mt <= k < mv -> fv k = dv) -> RelP (mkseq fv mv) (mkseq ft mt).
proof: Proof. move=> Hk Hv1 Hv2 k; rewrite !nth_mkseq_dflt. do 2![case: ifP]=> A B. - exact: H0. - by rewrite -(Hv1 k) // B ltnNge A. - by rewrite (Hv2 k) // A ltnNge B. - exact: Hk. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2