proposition: Lemma INJP_INJ {A : Type'} : forall f1 : nat -> A -> Prop, forall f1' : nat -> A -> Prop, forall f2 : nat -> A -> Prop, forall f2' : nat -> A -> Prop, ((@INJP A f1 f2) = (@INJP A f1' f2')) = ((f1 = f1') /\ (f2 = f2')).
proof: Proof. intros f1 f1' f2 f2'. apply prop_ext. 2: intros [e1 e2]; subst; reflexivity. intro e. assert (e1: forall x a, INJP f1 f2 x a = INJP f1' f2' x a). intros x a. rewrite e. reflexivity. split; apply fun_ext; intro x; apply fun_ext; intro a. generalize (e1 (S (2 * x)) a). unfold INJP, NUMLEFT, NUMRIGHT. rewrite even_succ, odd_double, !COND_True, S_minus_1, DIV_MULT. auto. lia. generalize (e1 (2 * x) a). unfold INJP, NUMLEFT, NUMRIGHT. rewrite even_double, !COND_False, DIV_MULT. auto. lia. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance