proposition: Lemma nds_induction_prop2 (f := nds_example) : [/\ forall i, natp i -> f \0c i = \1o, forall i, natp i -> f \1c i = \1o & forall n, natp n -> \1c <c n -> let k := nds_k_of n in same_below (f n) (nds_merge k (f (n -c k))) n].
proof: Proof. rewrite /f/nds_example /nds_example_set. set cstf := Lg Nat (fun _ : Set => \1o). set T := (fun k t : Set => Lg Nat (nds_merge k (Vg t))). move: (nds_induction_prop cstf cstf T). set g := nds_induction cstf cstf T. move => [p1 p2 p3]; rewrite p1 p2; split. by rewrite /cstf => i iN; rewrite LgV. by rewrite /cstf => i iN; rewrite LgV. move => n nN ln2 i lin; move: (NS_lt_nat lin nN) => iN. by rewrite (p3 _ nN ln2) /T !LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)