proposition: Lemma parent_dec: forall i, i > root_idx -> parent i < i.
proof: Proof. intros. destruct i. inversion H. destruct i. constructor. etransitivity. apply lt_div2; lia. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset