proposition: Lemma behead_rcons {T : Type} (s : seq T) (t : T) : (0 < size s)%nat -> behead (rcons s t) = rcons (behead s) t.
proof: Proof. case: s t => // t Hi ; contradict Hi ; apply Nat.nlt_0_r. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)