proposition: Remark cPairInjHelp : forall a b c d : nat, cPair a b = cPair c d -> a + b = c + d.
proof: Proof. assert (H: forall a b : nat, a < b -> a + sumToN a < sumToN b). { simple induction b. - intros H; elim (Nat.nlt_0_r _ H). - intros n H H0; simpl in |- *. assert (H1: a <= n) by (apply Compat815.lt_n_Sm_le; assumption). rewrite Nat.lt_eq_cases in H1; destruct H1. + apply Nat.lt_trans with (sumToN n). * auto. * apply Compat815.le_lt_n_Sm. rewrite Nat.add_comm; apply le_add_r. + rewrite H1. apply Nat.lt_succ_diag_r . } unfold cPair in |- *; assert (H0: forall a b c d : nat, a <= c -> b <= d -> a + sumToN c = b + sumToN d -> c = d). { intros a b c d H0 H1 H2; induction (le_gt_cases c d). - induction (Compat815.le_lt_or_eq _ _ H3). + assert (H5: a + sumToN c < sumToN d). { apply Nat.le_lt_trans with (c + sumToN c); [| auto]. now apply Nat.add_le_mono_r; auto. } rewrite H2 in H5; elim (Compat815.lt_not_le _ _ H5). rewrite Nat.add_comm;apply le_add_r. + auto. - assert (H4: b + sumToN d < sumToN c). { apply Nat.le_lt_trans with (d + sumToN d). - apply Nat.add_le_mono_r; auto. - auto. } rewrite <- H2 in H4; elim (Compat815.lt_not_le _ _ H4). rewrite add_comm; apply le_add_r. } intros; eapply H0. - apply Nat.le_add_r. - apply Nat.le_add_r. - auto. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec)