proposition: Lemma left_child_monotone: forall i j, i < j -> left_child i < left_child j.
proof: Proof. unfold left_child. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset