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