proposition: Lemma tree_ind (p: property): (forall n, natp n -> p (Tb n)) -> (forall x, treep x -> p x -> p (Tp x)) -> (forall x x', treep x -> treep x' -> p x -> p x' -> p(Tx x x')) -> (forall x, treep x -> p x).
proof: Proof. move => ha hb hc x xt; move: (NS_tdepth xt) => ns. move: (cleR (CS_nat ns)); move: ns. move: {1 3}(tdepth x) => m mn; move: m mn x xt; apply: Nat_induction. move => x xt /cle0 => dz. by move: (tdepth4 xt dz) => /tset_baseP [n nN ->]; apply: ha. move => n nN Hrec x xt /cle_eqVlt []; last by move/(cltSleP nN); apply: Hrec. case/(tdepth_prop xt nN). by move=>[y [ys dy ->]]; apply: hb => //; apply: Hrec. move => [y [z [ya za hy hz ->]]]. by apply: hc => //; apply: Hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)