proposition: Theorem inb_antisym : forall t1 t2 : btree, inb t1 t2 -> inb t2 t1 -> t1 = t2.
proof: Proof. intros t1 t2 H; elim H; auto. intros t t0 t3 H0 H1 H2. absurd (number_of_nodes (node t0 t3) <= number_of_nodes t). rewrite H1; simpl in |- *; auto with arith. apply inb_trans with (2 := H2); auto. apply number_of_nodes_inb_le; auto. intros t t0 t3 H0 H1 H2. absurd (number_of_nodes (node t0 t3) <= number_of_nodes t). rewrite H1; simpl in |- *; auto with arith. apply inb_trans with (2 := H2); auto. apply number_of_nodes_inb_le; auto. Qed.
imports: Coq(ArithRing ListDec)