proposition: Lemma size_nat_monotone p q : p<q -> (size_nat p <= size_nat q)%nat.
proof: Proof. assert (le0 : forall n, (0<=n)%nat) by (intro n; induction n; auto). assert (leS : forall n m, (n<=m -> S n <= S m)%nat) by (induction 1; auto). revert q. induction p as [p IHp|p IHp|]; intro q; destruct q as [q|q|]; simpl; intros H; auto; easy || apply leS; red in H; simpl_compare_in H. - apply IHp. red. now destruct (p?=q). - destruct (compare_spec p q); subst; now auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef