proposition: Lemma rcons_dec {T : Type} (P : seq T -> Type) : (P [::]) -> (forall s t, P (rcons s t)) -> forall s, P s.
proof: Proof. move => H0 Hr ; case => [| h s] //. have: ({s0 : _&{ t0 | h::s = rcons s0 t0}}) ; [| case => s0 [t0 H]]. elim: s h => [| h s IH] h0. exists [::] ; by exists h0. case: (IH h) => s0 [t0 H] ; exists (h0::s0) ; exists t0 ; by rewrite rcons_cons -H. by rewrite H. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)