proposition: Lemma pa6 (a b : Term) : SysPrf PA (a * Succ b = a * b + a)%nt.
proof: Proof. set (m := fun x : nat => match x with | O => a | S _ => b end) in *. replace (a * Succ b = a * b + a)%nt with (subAllFormula LNT (v#0 * Succ (v#1) = v#0 * v#1 + v#0)%nt (fun x : nat => match le_lt_dec 2 x with | left _ => var x | right _ => m x end)). - apply (subAllCloseFrom LNT). simpl in |- *. apply Axm; repeat (try right; constructor) || left. - simpl in |- *. induction (le_lt_dec 2 0). + lia. + induction (le_lt_dec 2 1). * lia. * reflexivity. Qed.
imports: Coq(Arith Lia Ensembles Decidable) hydras.Ackermann(folProp subAll folLogic3) hydras.Ackermann(NewNotations)