proposition: Lemma trans_dec_succ y: trans_dec_set y -> trans_dec_set (osucc y).
proof: Proof. move => [tsy dsy]; split. apply: osucc_prop; first by apply:setU1_r. by move => z zy t /(tsy _ zy) ty; apply:setU1_r. exact:(osucc_prop (irreflexive_decent dsy) dsy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)