proposition: Lemma codom_ux_rcons (f : {ffun 'I_n -> A}) (i : 'I_n) : &:(fgraph f) `]-oo, i : nat] = rcons (&:(fgraph f) `]-oo, i : nat[) (f i).
proof: Proof. by rewrite slice_xR // slice_uu onth_codom. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)