proposition: Lemma partition_join_start : forall H, partition_join_fun 0 H [=] a.
proof: Proof. intro. unfold partition_join_fun in |- *. elim (le_lt_dec 0 n); intro; simpl in |- *. apply start. exfalso; apply (Nat.nlt_0_r _ b0). Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)