proposition: Lemma right_child_root: forall i, right_child i > root_idx.
proof: Proof. unfold right_child, root_idx. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset