proposition: Lemma left_child_parent_odd: forall i, odd i -> left_child (parent i) = i.
proof: Proof. unfold left_child, parent. intros. inversion H. replace (S n - 1) with n by lia. simpl. f_equal. rewrite even_double; auto. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset