proposition: Lemma left_child_S_right_child: forall i, S (left_child i) = right_child i.
proof: Proof. unfold right_child. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset