proposition: Lemma nf_b_cons_eq a n b : nf_b (cons a n b) = nf_b a && nf_b b && bool_decide (lt b (phi0 a)).
proof: Proof. rewrite bool_eq_iff; generalize (nf_cons_iff a n b); unfold nf; intro H; rewrite H. destruct (decide (lt b (phi0 a))) as [Hdec|Hdec]. - pose proof Hdec as Heq. rewrite <- (bool_decide_eq_true _) in Heq. split; case (nf_b a); case (nf_b b); cbn; auto with bool; intros H0; decompose [and] H0; try discriminate. - pose proof Hdec as Heq. rewrite <- (bool_decide_eq_false _) in Heq. rewrite Heq. split; intro H0; repeat rewrite andb_true_iff in H0; decompose [and] H0; [congruence|]. rewrite andb_false_r in H0. discriminate. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)