proposition: Lemma max_arity_nth : forall le vars k d, max_arity_list le vars = true -> k < length le -> max_arity (nth k le d) vars = true.
proof: Proof. induction le ; try easy. intros vars k d H Hk. simpl in H. apply andb_prop in H. destruct H as [Ha Hle]. destruct k as [|k] ; try easy. apply IHle with (1 := Hle). now simpl in Hk; rewrite <-Nat.succ_lt_mono in Hk. Qed.
imports: Coq(ZArith Reals List Psatz) Xreal Tree