proposition: Lemma partition_join_prf1 : forall i j : nat, i = j -> forall Hi Hj, partition_join_fun i Hi [=] partition_join_fun j Hj.
proof: Proof. intros. unfold partition_join_fun in |- *. elim (le_lt_dec i n); elim (le_lt_dec j n); intros; simpl in |- *. apply prf1; auto. exfalso; apply Nat.le_ngt with i n. assumption. rewrite H; assumption. exfalso; apply Nat.le_ngt with j n. assumption. rewrite <- H; assumption. apply prf1; auto. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)