proposition: Theorem ltb_lt : forall n m, n << m = true <-> n < m.
proof: Proof. double_induct n m. - cases m. + rewrite ltb_0. split; intro H; [discriminate H | false_hyp H nlt_0_r]. + intro n. rewrite ltb_0_succ. split; intro; [apply lt_0_succ | reflexivity]. - intro n. rewrite ltb_0. split; intro H; [discriminate | false_hyp H nlt_0_r]. - intros n m. rewrite succ_ltb_mono. now rewrite <- succ_lt_mono. Qed.
imports: Bool RelationPairs NStrongRec