proposition: Lemma right_child_parent_even: forall i, i > root_idx -> even i -> right_child (parent i) = i.
proof: Proof. unfold right_child, left_child, parent, root_idx. intros. inversion H0. lia. replace (S n - 1) with n by lia. simpl. f_equal. rewrite (odd_double n) at 3; auto. unfold double. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset